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

Theorem excom 2206
Description: Theorem 19.11 of [Margaris] p. 89. (Contributed by NM, 5-Aug-1993.) Remove dependencies on ax-5 2005, ax-6 2069, ax-7 2105, ax-10 2183, ax-12 2211. (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 2201 . . 3 (∀𝑥𝑦 ¬ 𝜑 ↔ ∀𝑦𝑥 ¬ 𝜑)
21notbii 311 . 2 (¬ ∀𝑥𝑦 ¬ 𝜑 ↔ ¬ ∀𝑦𝑥 ¬ 𝜑)
3 2exnaln 1923 . 2 (∃𝑥𝑦𝜑 ↔ ¬ ∀𝑥𝑦 ¬ 𝜑)
4 2exnaln 1923 . 2 (∃𝑦𝑥𝜑 ↔ ¬ ∀𝑦𝑥 ¬ 𝜑)
52, 3, 43bitr4i 294 1 (∃𝑥𝑦𝜑 ↔ ∃𝑦𝑥𝜑)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 197  wal 1650  wex 1874
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-11 2198
This theorem depends on definitions:  df-bi 198  df-ex 1875
This theorem is referenced by:  excomim  2207  excom13  2208  exrot3  2209  ee4anv  2348  sbel2x  2551  2sb8e  2559  2euex  2666  2eu4  2678  rexcomf  3244  gencbvex  3403  euind  3552  sbccomlem  3667  opelopabsbALT  5145  elvvv  5346  dmuni  5502  dm0rn0  5510  dmcosseq  5556  elresOLD  5611  rnco  5827  coass  5840  oprabid  6873  dfoprab2  6899  uniuni  7169  opabex3d  7343  opabex3  7344  frxp  7489  domen  8173  xpassen  8261  scott0  8964  dfac5lem1  9197  dfac5lem4  9200  cflem  9321  ltexprlem1  10111  ltexprlem4  10114  fsumcom2  14792  fprodcom2  14999  gsumval3eu  18571  dprd2d2  18710  cnvoprabOLD  29882  eldm3  32028  dfdm5  32051  dfrn5  32052  elfuns  32398  dfiota3  32406  brimg  32420  funpartlem  32425  bj-rexcom4  33226  bj-restuni  33410  sbccom2lem  34282  diblsmopel  37059  dicelval3  37068  dihjatcclem4  37309  pm11.6  39198  ax6e2ndeq  39369  e2ebind  39373  ax6e2ndeqVD  39729  e2ebindVD  39732  e2ebindALT  39749  ax6e2ndeqALT  39751  elsprel  42326  eliunxp2  42713
  Copyright terms: Public domain W3C validator