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

Theorem excom 2167
 Description: Theorem 19.11 of [Margaris] p. 89. (Contributed by NM, 5-Aug-1993.) Remove dependencies on ax-5 1911, ax-6 1970, ax-7 2015, ax-10 2143, ax-12 2176. (Revised by Wolf Lammen, 8-Jan-2018.) (Proof shortened by Wolf Lammen, 22-Aug-2020.)
Assertion
Ref Expression
excom (∃𝑥𝑦𝜑 ↔ ∃𝑦𝑥𝜑)

Proof of Theorem excom
StepHypRef Expression
1 alcom 2161 . . 3 (∀𝑥𝑦 ¬ 𝜑 ↔ ∀𝑦𝑥 ¬ 𝜑)
21notbii 323 . 2 (¬ ∀𝑥𝑦 ¬ 𝜑 ↔ ¬ ∀𝑦𝑥 ¬ 𝜑)
3 2exnaln 1830 . 2 (∃𝑥𝑦𝜑 ↔ ¬ ∀𝑥𝑦 ¬ 𝜑)
4 2exnaln 1830 . 2 (∃𝑦𝑥𝜑 ↔ ¬ ∀𝑦𝑥 ¬ 𝜑)
52, 3, 43bitr4i 306 1 (∃𝑥𝑦𝜑 ↔ ∃𝑦𝑥𝜑)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   ↔ wb 209  ∀wal 1536  ∃wex 1781 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-11 2159 This theorem depends on definitions:  df-bi 210  df-ex 1782 This theorem is referenced by:  excomim  2168  excom13  2169  exrot3  2170  ee4anv  2364  2sb8ev  2367  sbel2x  2490  2sb8e  2555  2euexv  2696  2euex  2706  2eu4  2719  rexcom4  3215  rexcomOLD  3312  rexcomf  3314  cgsex4gOLD  3490  gencbvex  3500  euind  3666  sbccomlem  3802  opelopabsbALT  5384  elvvv  5595  dmuni  5751  dm0rn0  5763  dmcosseq  5813  rnco  6076  coass  6089  oprabidw  7170  oprabid  7171  dfoprab2  7195  uniuni  7468  opabex3d  7652  opabex3rd  7653  opabex3  7654  frxp  7807  domen  8509  xpassen  8598  scott0  9303  dfac5lem1  9538  dfac5lem4  9541  cflem  9661  ltexprlem1  10451  ltexprlem4  10454  fsumcom2  15125  fprodcom2  15334  gsumval3eu  19021  dprd2d2  19163  cnvoprabOLD  30486  eldm3  33111  dfdm5  33130  dfrn5  33131  elfuns  33490  dfiota3  33498  brimg  33512  funpartlem  33517  bj-19.12  34206  bj-nnflemee  34208  bj-restuni  34513  sbccom2lem  35561  diblsmopel  38466  dicelval3  38475  dihjatcclem4  38716  19.9dev  39393  pm11.6  41093  ax6e2ndeq  41262  e2ebind  41266  ax6e2ndeqVD  41612  e2ebindVD  41615  e2ebindALT  41632  ax6e2ndeqALT  41634  ich2ex  43982  ichexmpl1  43983  elsprel  43989  eliunxp2  44732
 Copyright terms: Public domain W3C validator