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

Theorem excom 1798
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 1797 . 2  |-  ( E. x E. y ph  ->  E. y E. x ph )
2 excomim 1797 . 2  |-  ( E. y E. x ph  ->  E. x E. y ph )
31, 2impbii 180 1  |-  ( E. x E. y ph  <->  E. y E. x ph )
Colors of variables: wff set class
Syntax hints:    <-> wb 176   E.wex 1531
This theorem is referenced by:  excom13  1829  exrot3  1830  ee4anv  1868  2exsb  2084  2euex  2228  2eu1  2236  2eu4  2239  rexcomf  2712  gencbvex  2843  euind  2965  sbccomlem  3074  opelopabsbOLD  4289  uniuni  4543  elvvv  4765  dmuni  4904  dm0rn0  4911  dmcosseq  4962  elres  5006  rnco  5195  coass  5207  opabex3  5785  oprabid  5898  dfoprab2  5911  frxp  6241  domen  6891  xpassen  6972  scott0  7572  dfac5lem1  7766  dfac5lem4  7769  cflem  7888  ltexprlem1  8676  ltexprlem4  8679  fsumcom2  12253  gsumval3eu  15206  dprd2d2  15295  eldm3  24190  dfdm5  24203  dfrn5  24204  dfiota3  24533  brimg  24547  brsuccf  24551  funpartlem  24552  pm11.6  27694  opabex3d  28190  a9e2ndeq  28624  e2ebind  28628  a9e2ndeqVD  29001  e2ebindVD  29004  e2ebindALT  29022  a9e2ndeqALT  29024  diblsmopel  31983  dicelval3  31992  dihjatcclem4  32233
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727
This theorem depends on definitions:  df-bi 177  df-tru 1310  df-ex 1532  df-nf 1535
  Copyright terms: Public domain W3C validator