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  2364  ee4anv  2381  ee4anvOLD  2382  2sb8ef  2386  sbel2x  2504  2sb8e  2560  2euexv  2657  2euex  2667  2eu4  2680  rexcom4  3290  rexcomf  3302  gencbvex  3507  euind  3682  elvvv  5727  dmuni  5896  dm0rn0OLD  5907  cnvopab  6131  rncoOLD  6253  coass  6266  oprabidw  7449  oprabid  7450  dfoprab2  7476  uniuni  7774  opabex3d  7975  opabex3rd  7976  opabex3  7977  frxp  8136  domen  8981  xpassen  9083  scott0b  9930  scott0OLD  9931  dfac5lem1  10195  ltexprlem1  11114  ltexprlem4  11117  fsumcom2  15933  fprodcom2  16144  gsumval3eu  20111  dprd2d2  20253  eldm3  36505  dfdm5  36517  dfrn5  36518  elfuns  36657  dfiota3  36665  brimg  36679  funpartlem  36686  bj-19.12  37605  bj-nnflemee  37669  bj-restuni  37998  sbccom2lem  39036  dmqsblocks  39879  diblsmopel  42208  dicelval3  42217  dihjatcclem4  42458  nfe2  43247  19.9dev  43249  nnoeomeqom  44298  pm11.6  45361  ax6e2ndeq  45527  e2ebind  45531  ax6e2ndeqVD  45876  e2ebindVD  45879  e2ebindALT  45896  ax6e2ndeqALT  45898  ich2ex  48519  ichexmpl1  48520  elsprel  48526  eliunxp2  49415