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  2338  ee4anv  2355  ee4anvOLD  2356  2sb8ef  2360  sbel2x  2478  2sb8e  2534  2euexv  2631  2euex  2641  2eu4  2655  rexcom4  3264  rexcomf  3276  gencbvex  3487  euind  3670  sbccomlemOLD  3808  elvvv  5707  dmuni  5869  dm0rn0OLD  5880  dmcosseqOLDOLD  5935  cnvopab  6100  rncoOLD  6217  coass  6230  oprabidw  7398  oprabid  7399  dfoprab2  7425  uniuni  7716  opabex3d  7918  opabex3rd  7919  opabex3  7920  frxp  8076  domen  8908  xpassen  9009  scott0  9810  dfac5lem1  10045  dfac5lem4OLD  10050  cflemOLD  10168  ltexprlem1  10959  ltexprlem4  10962  fsumcom2  15736  fprodcom2  15949  gsumval3eu  19879  dprd2d2  20021  eldm3  35943  dfdm5  35955  dfrn5  35956  elfuns  36095  dfiota3  36103  brimg  36117  funpartlem  36124  bj-19.12  37020  bj-nnflemee  37084  bj-restuni  37409  sbccom2lem  38445  dmqsblocks  39288  diblsmopel  41617  dicelval3  41626  dihjatcclem4  41867  nfe2  42654  19.9dev  42656  nnoeomeqom  43740  pm11.6  44819  ax6e2ndeq  44986  e2ebind  44990  ax6e2ndeqVD  45335  e2ebindVD  45338  e2ebindALT  45355  ax6e2ndeqALT  45357  ich2ex  47928  ichexmpl1  47929  elsprel  47935  eliunxp2  48810