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

Theorem excom 1748
Description: Theorem 19.11 of [Margaris] p. 89. Revised to remove dependency on ax-11 1753, ax-6 1736, ax-9 1661, ax-8 1682 and ax-17 1623. (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 1744 . . . 4  |-  ( A. x A. y  -.  ph  <->  A. y A. x  -.  ph )
21notbii 288 . . 3  |-  ( -. 
A. x A. y  -.  ph  <->  -.  A. y A. x  -.  ph )
3 exnal 1580 . . 3  |-  ( E. x  -.  A. y  -.  ph  <->  -.  A. x A. y  -.  ph )
4 exnal 1580 . . 3  |-  ( E. y  -.  A. x  -.  ph  <->  -.  A. y A. x  -.  ph )
52, 3, 43bitr4i 269 . 2  |-  ( E. x  -.  A. y  -.  ph  <->  E. y  -.  A. x  -.  ph )
6 df-ex 1548 . . 3  |-  ( E. y ph  <->  -.  A. y  -.  ph )
76exbii 1589 . 2  |-  ( E. x E. y ph  <->  E. x  -.  A. y  -.  ph )
8 df-ex 1548 . . 3  |-  ( E. x ph  <->  -.  A. x  -.  ph )
98exbii 1589 . 2  |-  ( E. y E. x ph  <->  E. y  -.  A. x  -.  ph )
105, 7, 93bitr4i 269 1  |-  ( E. x E. y ph  <->  E. y E. x ph )
Colors of variables: wff set class
Syntax hints:   -. wn 3    <-> wb 177   A.wal 1546   E.wex 1547
This theorem is referenced by:  excomim  1749  excom13  1750  exrot3  1751  ee4anv  1929  2exsb  2159  2euex  2303  2eu1  2311  2eu4  2314  rexcomf  2803  gencbvex  2934  euind  3057  sbccomlem  3167  opelopabsbOLD  4397  uniuni  4649  elvvv  4870  dmuni  5012  dm0rn0  5019  dmcosseq  5070  elres  5114  rnco  5309  coass  5321  opabex3d  5921  opabex3  5922  oprabid  6037  dfoprab2  6053  frxp  6385  domen  7050  xpassen  7131  scott0  7736  dfac5lem1  7930  dfac5lem4  7933  cflem  8052  ltexprlem1  8839  ltexprlem4  8842  fsumcom2  12478  gsumval3eu  15433  dprd2d2  15522  usgraedg4  21265  eldm3  25136  dfdm5  25149  dfrn5  25150  dfiota3  25479  brimg  25493  brsuccf  25497  funpartlem  25498  pm11.6  27253  a9e2ndeq  27982  e2ebind  27986  a9e2ndeqVD  28355  e2ebindVD  28358  e2ebindALT  28376  a9e2ndeqALT  28378  diblsmopel  31337  dicelval3  31346  dihjatcclem4  31587
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-7 1741
This theorem depends on definitions:  df-bi 178  df-ex 1548
  Copyright terms: Public domain W3C validator