Theorem excom 2199

Description: Theorem 19.11 of [Margaris] p. 89. (Contributed by NM, 5-Aug-1993.) Remove dependencies on ax-5 1943, ax-6 2000, ax-7 2041, ax-10 2178, ax-12 2213. (Revised by Wolf Lammen, 8-Jan-2018.) (Proof shortened by Wolf Lammen, 22-Aug-2020.)

Assertion

Ref	Expression
excom	⊢ (∃𝑥∃𝑦𝜑 ↔ ∃𝑦∃𝑥𝜑)

Proof of Theorem excom

Step	Hyp	Ref	Expression
1		alcom 2196	. . 3 ⊢ (∀𝑥∀𝑦 ¬ 𝜑 ↔ ∀𝑦∀𝑥 ¬ 𝜑)
2	1	notbii 323	. 2 ⊢ (¬ ∀𝑥∀𝑦 ¬ 𝜑 ↔ ¬ ∀𝑦∀𝑥 ¬ 𝜑)
3		2exnaln 1862	. 2 ⊢ (∃𝑥∃𝑦𝜑 ↔ ¬ ∀𝑥∀𝑦 ¬ 𝜑)
4		2exnaln 1862	. 2 ⊢ (∃𝑦∃𝑥𝜑 ↔ ¬ ∀𝑦∀𝑥 ¬ 𝜑)
5	2, 3, 4	3bitr4i 306	1 ⊢ (∃𝑥∃𝑦𝜑 ↔ ∃𝑦∃𝑥𝜑)

This proof depends on syntax axioms:  ¬ wn 3   ↔ wb 209  ∀wal 1568  ∃wex 1812

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-11 2194

This proof depends on definitions:  df-bi 210  df-ex 1813

This theorem is used by:  excomim  2200  excom13  2201  exrot3  2202  eeor  2363  ee4anv  2380  ee4anvOLD  2381  2sb8ef  2385  sbel2x  2503  2sb8e  2559  2euexv  2656  2euex  2666  2eu4  2679  rexcom4  3289  rexcomf  3301  gencbvex  3506  euind  3682  elvvv  5731  dmuni  5898  dm0rn0OLD  5909  cnvopab  6131  rncoOLD  6249  coass  6262  oprabidw  7444  oprabid  7445  dfoprab2  7471  uniuni  7761  opabex3d  7962  opabex3rd  7963  opabex3  7964  frxp  8124  domen  8967  xpassen  9069  scott0b  9876  scott0OLD  9877  dfac5lem1  10126  ltexprlem1  11045  ltexprlem4  11048  fsumcom2  15860  fprodcom2  16071  gsumval3eu  20031  dprd2d2  20173  eldm3  36340  dfdm5  36352  dfrn5  36353  elfuns  36492  dfiota3  36500  brimg  36514  funpartlem  36521  bj-19.12  37456  bj-nnflemee  37520  bj-restuni  37847  sbccom2lem  38872  dmqsblocks  39715  diblsmopel  42044  dicelval3  42053  dihjatcclem4  42294  nfe2  43083  19.9dev  43085  nnoeomeqom  44153  pm11.6  45216  ax6e2ndeq  45382  e2ebind  45386  ax6e2ndeqVD  45731  e2ebindVD  45734  e2ebindALT  45751  ax6e2ndeqALT  45753  ich2ex  48368  ichexmpl1  48369  elsprel  48375  eliunxp2  49264