ax-ex - brismu bridi

	brismu bridi		< Previous Next > Nearby theorems
Mirrors > Home > Home > Th. List > ax-ex

Axiom ax-ex 417

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. The apparent mismatch between metavariable types is required in order to evade the global distinctness requirement; this axiom holds even if {da} and {ko'a} are syntactically equivalent.

**Assertion**
Ref	Expression
ax-ex	⊢ su'o da zo'u da du ko'a

This axiom is referenced by: exv 418 equs4 454

W3C validator