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

Theorem excom 1757
Description: Theorem 19.11 of [Margaris] p. 89. Revised to remove dependency on ax-11 1762, ax-6 1745, ax-9 1667, ax-8 1688 and ax-17 1627. (Contributed by NM, 5-Aug-1993.) (Revised by Wolf Lammen, 8-Jan-2018.)
Assertion
Ref Expression
excom  |-  ( E. x E. y ph  <->  E. y E. x ph )

Proof of Theorem excom
StepHypRef Expression
1 alcom 1753 . . . 4  |-  ( A. x A. y  -.  ph  <->  A. y A. x  -.  ph )
21notbii 289 . . 3  |-  ( -. 
A. x A. y  -.  ph  <->  -.  A. y A. x  -.  ph )
3 exnal 1584 . . 3  |-  ( E. x  -.  A. y  -.  ph  <->  -.  A. x A. y  -.  ph )
4 exnal 1584 . . 3  |-  ( E. y  -.  A. x  -.  ph  <->  -.  A. y A. x  -.  ph )
52, 3, 43bitr4i 270 . 2  |-  ( E. x  -.  A. y  -.  ph  <->  E. y  -.  A. x  -.  ph )
6 df-ex 1552 . . 3  |-  ( E. y ph  <->  -.  A. y  -.  ph )
76exbii 1593 . 2  |-  ( E. x E. y ph  <->  E. x  -.  A. y  -.  ph )
8 df-ex 1552 . . 3  |-  ( E. x ph  <->  -.  A. x  -.  ph )
98exbii 1593 . 2  |-  ( E. y E. x ph  <->  E. y  -.  A. x  -.  ph )
105, 7, 93bitr4i 270 1  |-  ( E. x E. y ph  <->  E. y E. x ph )
Colors of variables: wff set class
Syntax hints:   -. wn 3    <-> wb 178   A.wal 1550   E.wex 1551
This theorem is referenced by:  excomim  1758  excom13  1759  exrot3  1760  ee4anv  1941  2exsb  2211  2euex  2355  2eu1  2363  2eu4  2366  rexcomf  2869  gencbvex  3000  euind  3123  sbccomlem  3233  opelopabsbOLD  4466  uniuni  4719  elvvv  4940  dmuni  5082  dm0rn0  5089  dmcosseq  5140  elres  5184  rnco  5379  coass  5391  opabex3d  5992  opabex3  5993  oprabid  6108  dfoprab2  6124  frxp  6459  domen  7124  xpassen  7205  scott0  7815  dfac5lem1  8009  dfac5lem4  8012  cflem  8131  ltexprlem1  8918  ltexprlem4  8921  fsumcom2  12563  gsumval3eu  15518  dprd2d2  15607  usgraedg4  21411  fprodcom2  25313  eldm3  25390  dfdm5  25405  dfrn5  25406  elfuns  25765  dfiota3  25773  brimg  25787  brsuccf  25791  funpartlem  25792  pm11.6  27582  a9e2ndeq  28720  e2ebind  28724  a9e2ndeqVD  29095  e2ebindVD  29098  e2ebindALT  29115  a9e2ndeqALT  29117  diblsmopel  32043  dicelval3  32052  dihjatcclem4  32293
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-7 1750
This theorem depends on definitions:  df-bi 179  df-ex 1552
  Copyright terms: Public domain W3C validator