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

Theorem excom 2163
Description: Theorem 19.11 of [Margaris] p. 89. (Contributed by NM, 5-Aug-1993.) Remove dependencies on ax-5 1914, ax-6 1972, ax-7 2012, ax-10 2138, ax-12 2172. (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 2157 . . 3 (∀𝑥𝑦 ¬ 𝜑 ↔ ∀𝑦𝑥 ¬ 𝜑)
21notbii 320 . 2 (¬ ∀𝑥𝑦 ¬ 𝜑 ↔ ¬ ∀𝑦𝑥 ¬ 𝜑)
3 2exnaln 1832 . 2 (∃𝑥𝑦𝜑 ↔ ¬ ∀𝑥𝑦 ¬ 𝜑)
4 2exnaln 1832 . 2 (∃𝑦𝑥𝜑 ↔ ¬ ∀𝑦𝑥 ¬ 𝜑)
52, 3, 43bitr4i 303 1 (∃𝑥𝑦𝜑 ↔ ∃𝑦𝑥𝜑)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 205  wal 1540  wex 1782
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-11 2155
This theorem depends on definitions:  df-bi 206  df-ex 1783
This theorem is referenced by:  excomim  2164  excom13  2165  exrot3  2166  eeor  2330  ee4anv  2348  2sb8ef  2353  sbel2x  2473  2sb8e  2534  2euexv  2632  2euex  2642  2eu4  2655  rexcom4  3274  rexcomf  3289  cgsex4gOLD  3494  gencbvex  3507  euind  3687  sbccomlem  3831  elvvv  5712  dmuni  5875  dm0rn0  5885  dmcosseq  5933  rnco  6209  coass  6222  oprabidw  7393  oprabid  7394  dfoprab2  7420  uniuni  7701  opabex3d  7903  opabex3rd  7904  opabex3  7905  frxp  8063  domen  8908  xpassen  9017  scott0  9829  dfac5lem1  10066  dfac5lem4  10069  cflem  10189  ltexprlem1  10979  ltexprlem4  10982  fsumcom2  15666  fprodcom2  15874  gsumval3eu  19688  dprd2d2  19830  cnvoprabOLD  31679  eldm3  34373  dfdm5  34386  dfrn5  34387  elfuns  34529  dfiota3  34537  brimg  34551  funpartlem  34556  bj-19.12  35255  bj-nnflemee  35257  bj-restuni  35597  sbccom2lem  36612  diblsmopel  39663  dicelval3  39672  dihjatcclem4  39913  19.9dev  40659  nnoeomeqom  41676  pm11.6  42746  ax6e2ndeq  42915  e2ebind  42919  ax6e2ndeqVD  43265  e2ebindVD  43268  e2ebindALT  43285  ax6e2ndeqALT  43287  ich2ex  45734  ichexmpl1  45735  elsprel  45741  eliunxp2  46483
  Copyright terms: Public domain W3C validator