Theorem excom 2168

Description: Theorem 19.11 of [Margaris] p. 89. (Contributed by NM, 5-Aug-1993.) Remove dependencies on ax-5 1912, ax-6 1969, ax-7 2010, ax-10 2147, ax-12 2185. (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 2165	. . 3 ⊢ (∀𝑥∀𝑦 ¬ 𝜑 ↔ ∀𝑦∀𝑥 ¬ 𝜑)
2	1	notbii 320	. 2 ⊢ (¬ ∀𝑥∀𝑦 ¬ 𝜑 ↔ ¬ ∀𝑦∀𝑥 ¬ 𝜑)
3		2exnaln 1831	. 2 ⊢ (∃𝑥∃𝑦𝜑 ↔ ¬ ∀𝑥∀𝑦 ¬ 𝜑)
4		2exnaln 1831	. 2 ⊢ (∃𝑦∃𝑥𝜑 ↔ ¬ ∀𝑦∀𝑥 ¬ 𝜑)
5	2, 3, 4	3bitr4i 303	1 ⊢ (∃𝑥∃𝑦𝜑 ↔ ∃𝑦∃𝑥𝜑)

Syntax hints:  ¬ wn 3   ↔ wb 206  ∀wal 1540  ∃wex 1781

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-11 2163

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

This theorem is referenced by:  excomim  2169  excom13  2170  exrot3  2171  eeor  2339  ee4anv  2356  ee4anvOLD  2357  2sb8ef  2361  sbel2x  2479  2sb8e  2535  2euexv  2632  2euex  2642  2eu4  2656  rexcom4  3265  rexcomf  3277  gencbvex  3488  euind  3671  sbccomlemOLD  3809  elvvv  5700  dmuni  5863  dm0rn0OLD  5874  dmcosseqOLDOLD  5929  cnvopab  6094  rncoOLD  6211  coass  6224  oprabidw  7391  oprabid  7392  dfoprab2  7418  uniuni  7709  opabex3d  7911  opabex3rd  7912  opabex3  7913  frxp  8069  domen  8901  xpassen  9002  scott0  9801  dfac5lem1  10036  dfac5lem4OLD  10041  cflemOLD  10159  ltexprlem1  10950  ltexprlem4  10953  fsumcom2  15727  fprodcom2  15940  gsumval3eu  19870  dprd2d2  20012  eldm3  35959  dfdm5  35971  dfrn5  35972  elfuns  36111  dfiota3  36119  brimg  36133  funpartlem  36140  bj-19.12  37036  bj-nnflemee  37100  bj-restuni  37425  sbccom2lem  38459  dmqsblocks  39302  diblsmopel  41631  dicelval3  41640  dihjatcclem4  41881  nfe2  42668  19.9dev  42670  nnoeomeqom  43758  pm11.6  44837  ax6e2ndeq  45004  e2ebind  45008  ax6e2ndeqVD  45353  e2ebindVD  45356  e2ebindALT  45373  ax6e2ndeqALT  45375  ich2ex  47940  ichexmpl1  47941  elsprel  47947  eliunxp2  48822