MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  excom Unicode version

Theorem excom 1765
Description: Theorem 19.11 of [Margaris] p. 89. (Contributed by NM, 5-Aug-1993.)
Assertion
Ref Expression
excom  |-  ( E. x E. y ph  <->  E. y E. x ph )

Proof of Theorem excom
StepHypRef Expression
1 excomim 1764 . 2  |-  ( E. x E. y ph  ->  E. y E. x ph )
2 excomim 1764 . 2  |-  ( E. y E. x ph  ->  E. x E. y ph )
31, 2impbii 182 1  |-  ( E. x E. y ph  <->  E. y E. x ph )
Colors of variables: wff set class
Syntax hints:    <-> wb 178   E.wex 1537
This theorem is referenced by:  excom13  1801  exrot3  1802  ee4anv  2057  2exsb  2091  2euex  2185  2eu1  2193  2eu4  2196  rexcomf  2661  gencbvex  2768  euind  2889  sbccomlem  2991  opelopabsbOLD  4166  uniuni  4418  elvvv  4656  dmuni  4795  dm0rn0  4802  dmcosseq  4853  elres  4897  rnco  5085  coass  5097  opabex3  5621  oprabid  5734  dfoprab2  5747  frxp  6077  domen  6761  xpassen  6841  scott0  7440  dfac5lem1  7634  dfac5lem4  7637  cflem  7756  ltexprlem1  8540  ltexprlem4  8543  fsumcom2  12114  gsumval3eu  15025  dprd2d2  15114  dfdm5  23300  dfrn5  23301  dfiota3  23636  brimg  23650  brsuccf  23654  funpartfun  23655  pm11.6  26757  a9e2ndeq  27018  e2ebind  27022  a9e2ndeqVD  27375  e2ebindVD  27378  e2ebindALT  27396  a9e2ndeqALT  27398  diblsmopel  30050  dicelval3  30059  dihjatcclem4  30300
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-4 1692
This theorem depends on definitions:  df-bi 179  df-tru 1315  df-ex 1538  df-nf 1540
  Copyright terms: Public domain W3C validator