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

Axiom ax-eq 383
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  384
  Copyright terms: Public domain W3C validator