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

Theorem excom 2039
Description: Theorem 19.11 of [Margaris] p. 89. (Contributed by NM, 5-Aug-1993.) Remove dependencies on ax-5 1836, ax-6 1885, ax-7 1932, ax-10 2016, ax-12 2044. (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 2034 . . 3 (∀𝑥𝑦 ¬ 𝜑 ↔ ∀𝑦𝑥 ¬ 𝜑)
21notbii 310 . 2 (¬ ∀𝑥𝑦 ¬ 𝜑 ↔ ¬ ∀𝑦𝑥 ¬ 𝜑)
3 2exnaln 1753 . 2 (∃𝑥𝑦𝜑 ↔ ¬ ∀𝑥𝑦 ¬ 𝜑)
4 2exnaln 1753 . 2 (∃𝑦𝑥𝜑 ↔ ¬ ∀𝑦𝑥 ¬ 𝜑)
52, 3, 43bitr4i 292 1 (∃𝑥𝑦𝜑 ↔ ∃𝑦𝑥𝜑)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 196  wal 1478  wex 1701
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-11 2031
This theorem depends on definitions:  df-bi 197  df-ex 1702
This theorem is referenced by:  excomim  2040  excom13  2041  exrot3  2042  ee4anv  2183  sbel2x  2458  2sb8e  2466  2euex  2543  2eu4  2555  rexcomf  3091  gencbvex  3240  euind  3380  sbccomlem  3495  opelopabsbALT  4954  elvvv  5149  dmuni  5304  dm0rn0  5312  dmcosseq  5357  elres  5404  rnco  5610  coass  5623  oprabid  6642  dfoprab2  6666  uniuni  6935  opabex3d  7106  opabex3  7107  frxp  7247  domen  7928  xpassen  8014  scott0  8709  dfac5lem1  8906  dfac5lem4  8909  cflem  9028  ltexprlem1  9818  ltexprlem4  9821  fsumcom2  14452  fsumcom2OLD  14453  fprodcom2  14658  fprodcom2OLD  14659  gsumval3eu  18245  dprd2d2  18383  cnvoprab  29382  eldm3  31413  dfdm5  31431  dfrn5  31432  elfuns  31717  dfiota3  31725  brimg  31739  funpartlem  31744  bj-rexcom4  32569  bj-restuni  32740  sbccom2lem  33600  diblsmopel  35979  dicelval3  35988  dihjatcclem4  36229  pm11.6  38113  ax6e2ndeq  38296  e2ebind  38300  ax6e2ndeqVD  38667  e2ebindVD  38670  e2ebindALT  38687  ax6e2ndeqALT  38689  elsprel  41043  eliunxp2  41430
  Copyright terms: Public domain W3C validator