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

Theorem excom 2162
Description: Theorem 19.11 of [Margaris] p. 89. (Contributed by NM, 5-Aug-1993.) Remove dependencies on ax-5 1910, ax-6 1967, ax-7 2007, ax-10 2141, ax-12 2177. (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 2159 . . 3 (∀𝑥𝑦 ¬ 𝜑 ↔ ∀𝑦𝑥 ¬ 𝜑)
21notbii 320 . 2 (¬ ∀𝑥𝑦 ¬ 𝜑 ↔ ¬ ∀𝑦𝑥 ¬ 𝜑)
3 2exnaln 1829 . 2 (∃𝑥𝑦𝜑 ↔ ¬ ∀𝑥𝑦 ¬ 𝜑)
4 2exnaln 1829 . 2 (∃𝑦𝑥𝜑 ↔ ¬ ∀𝑦𝑥 ¬ 𝜑)
52, 3, 43bitr4i 303 1 (∃𝑥𝑦𝜑 ↔ ∃𝑦𝑥𝜑)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wb 206  wal 1538  wex 1779
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-11 2157
This theorem depends on definitions:  df-bi 207  df-ex 1780
This theorem is referenced by:  excomim  2163  excom13  2164  exrot3  2165  eeor  2335  ee4anv  2353  ee4anvOLD  2354  2sb8ef  2359  sbel2x  2479  2sb8e  2535  2euexv  2631  2euex  2641  2eu4  2655  rexcom4  3288  rexcomf  3303  gencbvex  3541  euind  3730  sbccomlemOLD  3870  elvvv  5761  dmuni  5925  dm0rn0  5935  dmcosseqOLD  5988  cnvopab  6157  rnco  6272  coass  6285  oprabidw  7462  oprabid  7463  dfoprab2  7491  uniuni  7782  opabex3d  7990  opabex3rd  7991  opabex3  7992  frxp  8151  domen  9002  xpassen  9106  scott0  9926  dfac5lem1  10163  dfac5lem4OLD  10168  cflemOLD  10286  ltexprlem1  11076  ltexprlem4  11079  fsumcom2  15810  fprodcom2  16020  gsumval3eu  19922  dprd2d2  20064  eldm3  35761  dfdm5  35773  dfrn5  35774  elfuns  35916  dfiota3  35924  brimg  35938  funpartlem  35943  bj-19.12  36762  bj-nnflemee  36764  bj-restuni  37098  sbccom2lem  38131  diblsmopel  41173  dicelval3  41182  dihjatcclem4  41423  19.9dev  42253  nnoeomeqom  43325  pm11.6  44411  ax6e2ndeq  44579  e2ebind  44583  ax6e2ndeqVD  44929  e2ebindVD  44932  e2ebindALT  44949  ax6e2ndeqALT  44951  ich2ex  47455  ichexmpl1  47456  elsprel  47462  eliunxp2  48250
  Copyright terms: Public domain W3C validator