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

Theorem excom 1787
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 1786 . 2  |-  ( E. x E. y ph  ->  E. y E. x ph )
2 excomim 1786 . 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 1529
This theorem is referenced by:  excom13  1818  exrot3  1819  ee4anv  1857  2exsb  2074  2euex  2216  2eu1  2224  2eu4  2227  rexcomf  2700  gencbvex  2831  euind  2953  sbccomlem  3062  opelopabsbOLD  4272  uniuni  4526  elvvv  4748  dmuni  4887  dm0rn0  4894  dmcosseq  4945  elres  4989  rnco  5177  coass  5189  opabex3  5730  oprabid  5843  dfoprab2  5856  frxp  6186  domen  6870  xpassen  6951  scott0  7551  dfac5lem1  7745  dfac5lem4  7748  cflem  7867  ltexprlem1  8655  ltexprlem4  8658  fsumcom2  12231  gsumval3eu  15184  dprd2d2  15273  dfdm5  23533  dfrn5  23534  dfiota3  23869  brimg  23883  brsuccf  23887  funpartfun  23888  pm11.6  26990  a9e2ndeq  27596  e2ebind  27600  a9e2ndeqVD  27953  e2ebindVD  27956  e2ebindALT  27974  a9e2ndeqALT  27976  diblsmopel  30628  dicelval3  30637  dihjatcclem4  30878
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1534  ax-5 1545  ax-17 1604  ax-9 1637  ax-8 1645  ax-6 1704  ax-7 1709  ax-11 1716
This theorem depends on definitions:  df-bi 179  df-tru 1312  df-ex 1530  df-nf 1533
  Copyright terms: Public domain W3C validator