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

Theorem excom 2191
Description: Theorem 19.11 of [Margaris] p. 89. (Contributed by NM, 5-Aug-1993.) Remove dependencies on ax-5 1988, ax-6 2054, ax-7 2090, ax-10 2168, ax-12 2196. (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 2186 . . 3 (∀𝑥𝑦 ¬ 𝜑 ↔ ∀𝑦𝑥 ¬ 𝜑)
21notbii 309 . 2 (¬ ∀𝑥𝑦 ¬ 𝜑 ↔ ¬ ∀𝑦𝑥 ¬ 𝜑)
3 2exnaln 1905 . 2 (∃𝑥𝑦𝜑 ↔ ¬ ∀𝑥𝑦 ¬ 𝜑)
4 2exnaln 1905 . 2 (∃𝑦𝑥𝜑 ↔ ¬ ∀𝑦𝑥 ¬ 𝜑)
52, 3, 43bitr4i 292 1 (∃𝑥𝑦𝜑 ↔ ∃𝑦𝑥𝜑)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 196  wal 1630  wex 1853
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-11 2183
This theorem depends on definitions:  df-bi 197  df-ex 1854
This theorem is referenced by:  excomim  2192  excom13  2193  exrot3  2194  ee4anv  2329  sbel2x  2596  2sb8e  2604  2euex  2682  2eu4  2694  rexcomf  3235  gencbvex  3390  euind  3534  sbccomlem  3649  opelopabsbALT  5134  elvvv  5335  dmuni  5489  dm0rn0  5497  dmcosseq  5542  elres  5593  rnco  5802  coass  5815  oprabid  6840  dfoprab2  6866  uniuni  7136  opabex3d  7310  opabex3  7311  frxp  7455  domen  8134  xpassen  8219  scott0  8922  dfac5lem1  9136  dfac5lem4  9139  cflem  9260  ltexprlem1  10050  ltexprlem4  10053  fsumcom2  14704  fsumcom2OLD  14705  fprodcom2  14913  fprodcom2OLD  14914  gsumval3eu  18505  dprd2d2  18643  cnvoprabOLD  29807  eldm3  31958  dfdm5  31981  dfrn5  31982  elfuns  32328  dfiota3  32336  brimg  32350  funpartlem  32355  bj-rexcom4  33175  bj-restuni  33356  sbccom2lem  34242  diblsmopel  36962  dicelval3  36971  dihjatcclem4  37212  pm11.6  39094  ax6e2ndeq  39277  e2ebind  39281  ax6e2ndeqVD  39644  e2ebindVD  39647  e2ebindALT  39664  ax6e2ndeqALT  39666  elsprel  42235  eliunxp2  42622
  Copyright terms: Public domain W3C validator