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

Theorem excom 1759
Description: Theorem 19.11 of [Margaris] p. 89. Revised to remove dependency on ax-11 1764, ax-6 1747, ax-9 1669, ax-8 1690 and ax-17 1628. (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 1755 . . . 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  1760  excom13  1761  exrot3  1762  ee4anv  1944  2exsb  2216  2euex  2360  2eu1  2368  2eu4  2371  rexcomf  2874  gencbvex  3007  euind  3130  sbccomlem  3247  opelopabsbOLD  4498  uniuni  4751  elvvv  4972  dmuni  5114  dm0rn0  5121  dmcosseq  5172  elres  5216  rnco  5411  coass  5423  opabex3d  6025  opabex3  6026  oprabid  6141  dfoprab2  6157  frxp  6492  domen  7157  xpassen  7238  scott0  7848  dfac5lem1  8042  dfac5lem4  8045  cflem  8164  ltexprlem1  8951  ltexprlem4  8954  fsumcom2  12596  gsumval3eu  15551  dprd2d2  15640  usgraedg4  21444  fprodcom2  25343  eldm3  25420  dfdm5  25435  dfrn5  25436  elfuns  25795  dfiota3  25803  brimg  25817  brsuccf  25821  funpartlem  25822  pm11.6  27680  a9e2ndeq  28818  e2ebind  28822  a9e2ndeqVD  29195  e2ebindVD  29198  e2ebindALT  29215  a9e2ndeqALT  29217  diblsmopel  32143  dicelval3  32152  dihjatcclem4  32393
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 1752
This theorem depends on definitions:  df-bi 179  df-ex 1552
  Copyright terms: Public domain W3C validator