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

Axiom ax-eq 422
Description: Extensional definition of existential quantification in terms of universal quantification.
Assertion
Ref Expression
ax-eqganai 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  423
  Copyright terms: Public domain W3C validator