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

Theorem excom 1756
Description: Theorem 19.11 of [Margaris] p. 89. Revised to remove dependency on ax-11 1761, ax-6 1744, ax-9 1666, ax-8 1687 and ax-17 1626. (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 1752 . . . 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 1583 . . 3  |-  ( E. x  -.  A. y  -.  ph  <->  -.  A. x A. y  -.  ph )
4 exnal 1583 . . 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 1551 . . 3  |-  ( E. y ph  <->  -.  A. y  -.  ph )
76exbii 1592 . 2  |-  ( E. x E. y ph  <->  E. x  -.  A. y  -.  ph )
8 df-ex 1551 . . 3  |-  ( E. x ph  <->  -.  A. x  -.  ph )
98exbii 1592 . 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 1549   E.wex 1550
This theorem is referenced by:  excomim  1757  excom13  1758  exrot3  1759  ee4anv  1940  2exsb  2208  2euex  2352  2eu1  2360  2eu4  2363  rexcomf  2854  gencbvex  2985  euind  3108  sbccomlem  3218  opelopabsbOLD  4450  uniuni  4702  elvvv  4923  dmuni  5065  dm0rn0  5072  dmcosseq  5123  elres  5167  rnco  5362  coass  5374  opabex3d  5975  opabex3  5976  oprabid  6091  dfoprab2  6107  frxp  6442  domen  7107  xpassen  7188  scott0  7794  dfac5lem1  7988  dfac5lem4  7991  cflem  8110  ltexprlem1  8897  ltexprlem4  8900  fsumcom2  12541  gsumval3eu  15496  dprd2d2  15585  usgraedg4  21389  fprodcom2  25292  eldm3  25369  dfdm5  25382  dfrn5  25383  dfiota3  25713  brimg  25727  brsuccf  25731  funpartlem  25732  pm11.6  27501  a9e2ndeq  28399  e2ebind  28403  a9e2ndeqVD  28773  e2ebindVD  28776  e2ebindALT  28794  a9e2ndeqALT  28796  diblsmopel  31700  dicelval3  31709  dihjatcclem4  31950
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-7 1749
This theorem depends on definitions:  df-bi 178  df-ex 1551
  Copyright terms: Public domain W3C validator