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

Theorem excom 2151
Description: Theorem 19.11 of [Margaris] p. 89. (Contributed by NM, 5-Aug-1993.) Remove dependencies on ax-5 1905, ax-6 1963, ax-7 2003, ax-10 2129, ax-12 2166. (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 2148 . . 3 (∀𝑥𝑦 ¬ 𝜑 ↔ ∀𝑦𝑥 ¬ 𝜑)
21notbii 319 . 2 (¬ ∀𝑥𝑦 ¬ 𝜑 ↔ ¬ ∀𝑦𝑥 ¬ 𝜑)
3 2exnaln 1823 . 2 (∃𝑥𝑦𝜑 ↔ ¬ ∀𝑥𝑦 ¬ 𝜑)
4 2exnaln 1823 . 2 (∃𝑦𝑥𝜑 ↔ ¬ ∀𝑦𝑥 ¬ 𝜑)
52, 3, 43bitr4i 302 1 (∃𝑥𝑦𝜑 ↔ ∃𝑦𝑥𝜑)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 205  wal 1531  wex 1773
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-11 2146
This theorem depends on definitions:  df-bi 206  df-ex 1774
This theorem is referenced by:  excomim  2152  excom13  2153  exrot3  2154  eeor  2323  ee4anv  2341  2sb8ef  2346  sbel2x  2467  2sb8e  2523  2euexv  2619  2euex  2629  2eu4  2643  rexcom4  3275  rexcomf  3290  cgsex4gOLDOLD  3511  gencbvex  3525  euind  3716  sbccomlem  3860  elvvv  5753  dmuni  5917  dm0rn0  5927  dmcosseq  5976  cnvopab  6144  rnco  6258  coass  6271  oprabidw  7450  oprabid  7451  dfoprab2  7478  uniuni  7765  opabex3d  7970  opabex3rd  7971  opabex3  7972  frxp  8131  domen  8982  xpassen  9091  scott0  9911  dfac5lem1  10148  dfac5lem4  10151  cflem  10271  ltexprlem1  11061  ltexprlem4  11064  fsumcom2  15756  fprodcom2  15964  gsumval3eu  19871  dprd2d2  20013  cnvoprabOLD  32584  eldm3  35483  dfdm5  35496  dfrn5  35497  elfuns  35639  dfiota3  35647  brimg  35661  funpartlem  35666  bj-19.12  36366  bj-nnflemee  36368  bj-restuni  36704  sbccom2lem  37725  diblsmopel  40771  dicelval3  40780  dihjatcclem4  41021  19.9dev  41832  nnoeomeqom  42880  pm11.6  43968  ax6e2ndeq  44137  e2ebind  44141  ax6e2ndeqVD  44487  e2ebindVD  44490  e2ebindALT  44507  ax6e2ndeqALT  44509  ich2ex  46942  ichexmpl1  46943  elsprel  46949  eliunxp2  47580
  Copyright terms: Public domain W3C validator