ax-eq - brismu bridi

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

Axiom ax-eq 420

Description: Extensional definition of existential quantification in terms of universal quantification.

**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 421