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

Theorem excom 2029
 Description: Theorem 19.11 of [Margaris] p. 89. (Contributed by NM, 5-Aug-1993.) Remove dependencies on ax-5 1827, ax-6 1875, ax-7 1922, ax-10 2006, ax-12 2034. (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 2024 . . 3 (∀𝑥𝑦 ¬ 𝜑 ↔ ∀𝑦𝑥 ¬ 𝜑)
21notbii 309 . 2 (¬ ∀𝑥𝑦 ¬ 𝜑 ↔ ¬ ∀𝑦𝑥 ¬ 𝜑)
3 2exnaln 1746 . 2 (∃𝑥𝑦𝜑 ↔ ¬ ∀𝑥𝑦 ¬ 𝜑)
4 2exnaln 1746 . 2 (∃𝑦𝑥𝜑 ↔ ¬ ∀𝑦𝑥 ¬ 𝜑)
52, 3, 43bitr4i 291 1 (∃𝑥𝑦𝜑 ↔ ∃𝑦𝑥𝜑)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   ↔ wb 195  ∀wal 1473  ∃wex 1695 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-11 2021 This theorem depends on definitions:  df-bi 196  df-ex 1696 This theorem is referenced by:  excomim  2030  excom13  2031  exrot3  2032  ee4anv  2172  sbel2x  2447  2sb8e  2455  2euex  2532  2eu4  2544  rexcomf  3078  gencbvex  3223  euind  3360  sbccomlem  3475  opelopabsbALT  4909  elvvv  5101  dmuni  5256  dm0rn0  5263  dmcosseq  5308  elres  5355  rnco  5558  coass  5571  oprabid  6576  dfoprab2  6599  uniuni  6865  opabex3d  7037  opabex3  7038  frxp  7174  domen  7854  xpassen  7939  scott0  8632  dfac5lem1  8829  dfac5lem4  8832  cflem  8951  ltexprlem1  9737  ltexprlem4  9740  fsumcom2  14347  fsumcom2OLD  14348  fprodcom2  14553  fprodcom2OLD  14554  gsumval3eu  18128  dprd2d2  18266  usgraedg4  25916  cnvoprab  28886  eldm3  30905  dfdm5  30921  dfrn5  30922  elfuns  31192  dfiota3  31200  brimg  31214  funpartlem  31219  bj-rexcom4  32063  bj-restuni  32231  sbccom2lem  33099  diblsmopel  35478  dicelval3  35487  dihjatcclem4  35728  pm11.6  37614  ax6e2ndeq  37796  e2ebind  37800  ax6e2ndeqVD  38167  e2ebindVD  38170  e2ebindALT  38187  ax6e2ndeqALT  38189  eliunxp2  41905
 Copyright terms: Public domain W3C validator