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

Theorem excom 1752
Description: Theorem 19.11 of [Margaris] p. 89. Revised to remove dependency on ax-11 1757, ax-6 1740, ax-9 1662, ax-8 1683 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 1748 . . . 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  1753  excom13  1754  exrot3  1755  ee4anv  1936  2exsb  2182  2euex  2326  2eu1  2334  2eu4  2337  rexcomf  2827  gencbvex  2958  euind  3081  sbccomlem  3191  opelopabsbOLD  4423  uniuni  4675  elvvv  4896  dmuni  5038  dm0rn0  5045  dmcosseq  5096  elres  5140  rnco  5335  coass  5347  opabex3d  5948  opabex3  5949  oprabid  6064  dfoprab2  6080  frxp  6415  domen  7080  xpassen  7161  scott0  7766  dfac5lem1  7960  dfac5lem4  7963  cflem  8082  ltexprlem1  8869  ltexprlem4  8872  fsumcom2  12513  gsumval3eu  15468  dprd2d2  15557  usgraedg4  21359  fprodcom2  25261  eldm3  25333  dfdm5  25346  dfrn5  25347  dfiota3  25676  brimg  25690  brsuccf  25694  funpartlem  25695  pm11.6  27459  a9e2ndeq  28357  e2ebind  28361  a9e2ndeqVD  28730  e2ebindVD  28733  e2ebindALT  28751  a9e2ndeqALT  28753  diblsmopel  31654  dicelval3  31663  dihjatcclem4  31904
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 1745
This theorem depends on definitions:  df-bi 178  df-ex 1548
  Copyright terms: Public domain W3C validator