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  2060  2exsb  2094  2euex  2188  2eu1  2196  2eu4  2199  rexcomf  2672  gencbvex  2798  euind  2920  sbccomlem  3022  opelopabsbOLD  4231  uniuni  4485  elvvv  4723  dmuni  4862  dm0rn0  4869  dmcosseq  4920  elres  4964  rnco  5152  coass  5164  opabex3  5689  oprabid  5802  dfoprab2  5815  frxp  6145  domen  6829  xpassen  6910  scott0  7510  dfac5lem1  7704  dfac5lem4  7707  cflem  7826  ltexprlem1  8614  ltexprlem4  8617  fsumcom2  12188  gsumval3eu  15138  dprd2d2  15227  dfdm5  23487  dfrn5  23488  dfiota3  23823  brimg  23837  brsuccf  23841  funpartfun  23842  pm11.6  26944  a9e2ndeq  27362  e2ebind  27366  a9e2ndeqVD  27719  e2ebindVD  27722  e2ebindALT  27740  a9e2ndeqALT  27742  diblsmopel  30512  dicelval3  30521  dihjatcclem4  30762
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