ax-ex - brismu bridi

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

Axiom ax-ex 416

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 417 equs4 453

W3C validator