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

Theorem excom 1786
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 1785 . 2  |-  ( E. x E. y ph  ->  E. y E. x ph )
2 excomim 1785 . 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 1528
This theorem is referenced by:  excom13  1817  exrot3  1818  ee4anv  1856  2exsb  2071  2euex  2215  2eu1  2223  2eu4  2226  rexcomf  2699  gencbvex  2830  euind  2952  sbccomlem  3061  opelopabsbOLD  4273  uniuni  4527  elvvv  4749  dmuni  4888  dm0rn0  4895  dmcosseq  4946  elres  4990  rnco  5179  coass  5191  opabex3  5769  oprabid  5882  dfoprab2  5895  frxp  6225  domen  6875  xpassen  6956  scott0  7556  dfac5lem1  7750  dfac5lem4  7753  cflem  7872  ltexprlem1  8660  ltexprlem4  8663  fsumcom2  12237  gsumval3eu  15190  dprd2d2  15279  eldm3  24119  dfdm5  24132  dfrn5  24133  dfiota3  24462  brimg  24476  brsuccf  24480  funpartfun  24481  pm11.6  27591  a9e2ndeq  28325  e2ebind  28329  a9e2ndeqVD  28685  e2ebindVD  28688  e2ebindALT  28706  a9e2ndeqALT  28708  diblsmopel  31361  dicelval3  31370  dihjatcclem4  31611
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715
This theorem depends on definitions:  df-bi 177  df-tru 1310  df-ex 1529  df-nf 1532
  Copyright terms: Public domain W3C validator