Theorem excom 2173

Description: Theorem 19.11 of [Margaris] p. 89. (Contributed by NM, 5-Aug-1993.) Remove dependencies on ax-5 1917, ax-6 1974, ax-7 2015, ax-10 2152, ax-12 2189. (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 2170	. . 3 ⊢ (∀𝑥∀𝑦 ¬ 𝜑 ↔ ∀𝑦∀𝑥 ¬ 𝜑)
2	1	notbii 321	. 2 ⊢ (¬ ∀𝑥∀𝑦 ¬ 𝜑 ↔ ¬ ∀𝑦∀𝑥 ¬ 𝜑)
3		2exnaln 1836	. 2 ⊢ (∃𝑥∃𝑦𝜑 ↔ ¬ ∀𝑥∀𝑦 ¬ 𝜑)
4		2exnaln 1836	. 2 ⊢ (∃𝑦∃𝑥𝜑 ↔ ¬ ∀𝑦∀𝑥 ¬ 𝜑)
5	2, 3, 4	3bitr4i 304	1 ⊢ (∃𝑥∃𝑦𝜑 ↔ ∃𝑦∃𝑥𝜑)

Syntax hints:  ¬ wn 3   ↔ wb 207  ∀wal 1545  ∃wex 1786

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-11 2168

This theorem depends on definitions:  df-bi 208  df-ex 1787

This theorem is referenced by:  excomim  2174  excom13  2175  exrot3  2176  eeor  2342  ee4anv  2359  ee4anvOLD  2360  2sb8ef  2364  sbel2x  2482  2sb8e  2538  2euexv  2635  2euex  2645  2eu4  2658  rexcom4  3266  rexcomf  3278  gencbvex  3488  euind  3665  sbccomlemOLD  3802  elvvv  5694  dmuni  5856  dm0rn0OLD  5867  dmcosseqOLDOLD  5922  cnvopab  6087  rncoOLD  6204  coass  6217  oprabidw  7387  oprabid  7388  dfoprab2  7414  uniuni  7705  opabex3d  7907  opabex3rd  7908  opabex3  7909  frxp  8066  domen  8898  xpassen  8999  scott0  9801  dfac5lem1  10036  dfac5lem4OLD  10041  cflemOLD  10159  ltexprlem1  10950  ltexprlem4  10953  fsumcom2  15727  fprodcom2  15940  gsumval3eu  19870  dprd2d2  20012  eldm3  35989  dfdm5  36001  dfrn5  36002  elfuns  36141  dfiota3  36149  brimg  36163  funpartlem  36170  bj-19.12  37066  bj-nnflemee  37130  bj-restuni  37455  sbccom2lem  38491  dmqsblocks  39334  diblsmopel  41663  dicelval3  41672  dihjatcclem4  41913  nfe2  42700  19.9dev  42702  nnoeomeqom  43757  pm11.6  44836  ax6e2ndeq  45003  e2ebind  45007  ax6e2ndeqVD  45352  e2ebindVD  45355  e2ebindALT  45372  ax6e2ndeqALT  45374  ich2ex  47943  ichexmpl1  47944  elsprel  47950  eliunxp2  48825