ax-eq - brismu bridi

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

Axiom ax-eq 345

Description: Extensional definition of existential quantification in terms of universal quantification. Axiom ax-ie2 in [ILE] p. 0.

**Assertion**
Ref	Expression
ax-eq	⊢ ganai ro da zo'u ganai broda gi ro da zo'u broda gi go ro da zo'u ganai brode gi broda gi ganai su'o da zo'u brode gi broda

This axiom is referenced by: eqi 346