Home brismu bridi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >   Home  >  Th. List  >  ax-ex
Axiom ax-ex 342
Description: The axiom of existence: at least one element exists in the universe. This is necessary if we want to exclude the trivial empty model. Axiom ax-i9 in [ILE] p. 0.
Assertion
Ref Expression
ax-ex ⊢ su'o da zo'u da du de
Distinct variable group:   da ,de
This axiom is referenced by: (None)
  Copyright terms: Public domain W3C validator