Theorem excom 2160

Description: Theorem 19.11 of [Margaris] p. 89. (Contributed by NM, 5-Aug-1993.) Remove dependencies on ax-5 1908, ax-6 1965, ax-7 2005, ax-10 2139, ax-12 2175. (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 2157	. . 3 ⊢ (∀𝑥∀𝑦 ¬ 𝜑 ↔ ∀𝑦∀𝑥 ¬ 𝜑)
2	1	notbii 320	. 2 ⊢ (¬ ∀𝑥∀𝑦 ¬ 𝜑 ↔ ¬ ∀𝑦∀𝑥 ¬ 𝜑)
3		2exnaln 1826	. 2 ⊢ (∃𝑥∃𝑦𝜑 ↔ ¬ ∀𝑥∀𝑦 ¬ 𝜑)
4		2exnaln 1826	. 2 ⊢ (∃𝑦∃𝑥𝜑 ↔ ¬ ∀𝑦∀𝑥 ¬ 𝜑)
5	2, 3, 4	3bitr4i 303	1 ⊢ (∃𝑥∃𝑦𝜑 ↔ ∃𝑦∃𝑥𝜑)

Syntax hints:  ¬ wn 3   ↔ wb 206  ∀wal 1535  ∃wex 1776

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-11 2155

This theorem depends on definitions:  df-bi 207  df-ex 1777

This theorem is referenced by:  excomim  2161  excom13  2162  exrot3  2163  eeor  2334  ee4anv  2352  2sb8ef  2357  sbel2x  2477  2sb8e  2533  2euexv  2629  2euex  2639  2eu4  2653  rexcom4  3286  rexcomf  3301  gencbvex  3541  euind  3733  sbccomlemOLD  3879  elvvv  5764  dmuni  5928  dm0rn0  5938  dmcosseqOLD  5991  cnvopab  6160  rnco  6274  coass  6287  oprabidw  7462  oprabid  7463  dfoprab2  7491  uniuni  7781  opabex3d  7989  opabex3rd  7990  opabex3  7991  frxp  8150  domen  9001  xpassen  9105  scott0  9924  dfac5lem1  10161  dfac5lem4OLD  10166  cflemOLD  10284  ltexprlem1  11074  ltexprlem4  11077  fsumcom2  15807  fprodcom2  16017  gsumval3eu  19937  dprd2d2  20079  cnvoprabOLD  32738  eldm3  35741  dfdm5  35754  dfrn5  35755  elfuns  35897  dfiota3  35905  brimg  35919  funpartlem  35924  bj-19.12  36744  bj-nnflemee  36746  bj-restuni  37080  sbccom2lem  38111  diblsmopel  41154  dicelval3  41163  dihjatcclem4  41404  19.9dev  42232  nnoeomeqom  43302  pm11.6  44388  ax6e2ndeq  44557  e2ebind  44561  ax6e2ndeqVD  44907  e2ebindVD  44910  e2ebindALT  44927  ax6e2ndeqALT  44929  ich2ex  47393  ichexmpl1  47394  elsprel  47400  eliunxp2  48179