Theorem excom 2163

Description: Theorem 19.11 of [Margaris] p. 89. (Contributed by NM, 5-Aug-1993.) Remove dependencies on ax-5 1910, ax-6 1967, ax-7 2008, ax-10 2142, ax-12 2178. (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 2160	. . 3 ⊢ (∀𝑥∀𝑦 ¬ 𝜑 ↔ ∀𝑦∀𝑥 ¬ 𝜑)
2	1	notbii 320	. 2 ⊢ (¬ ∀𝑥∀𝑦 ¬ 𝜑 ↔ ¬ ∀𝑦∀𝑥 ¬ 𝜑)
3		2exnaln 1829	. 2 ⊢ (∃𝑥∃𝑦𝜑 ↔ ¬ ∀𝑥∀𝑦 ¬ 𝜑)
4		2exnaln 1829	. 2 ⊢ (∃𝑦∃𝑥𝜑 ↔ ¬ ∀𝑦∀𝑥 ¬ 𝜑)
5	2, 3, 4	3bitr4i 303	1 ⊢ (∃𝑥∃𝑦𝜑 ↔ ∃𝑦∃𝑥𝜑)

Syntax hints:  ¬ wn 3   ↔ wb 206  ∀wal 1538  ∃wex 1779

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-11 2158

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

This theorem is referenced by:  excomim  2164  excom13  2165  exrot3  2166  eeor  2332  ee4anv  2349  ee4anvOLD  2350  2sb8ef  2354  sbel2x  2472  2sb8e  2528  2euexv  2624  2euex  2634  2eu4  2648  rexcom4  3256  rexcomf  3269  gencbvex  3498  euind  3686  sbccomlemOLD  3824  elvvv  5699  dmuni  5861  dm0rn0  5871  dmcosseqOLDOLD  5925  cnvopab  6090  rnco  6205  coass  6218  oprabidw  7384  oprabid  7385  dfoprab2  7411  uniuni  7702  opabex3d  7907  opabex3rd  7908  opabex3  7909  frxp  8066  domen  8894  xpassen  8995  scott0  9801  dfac5lem1  10036  dfac5lem4OLD  10041  cflemOLD  10159  ltexprlem1  10949  ltexprlem4  10952  fsumcom2  15699  fprodcom2  15909  gsumval3eu  19801  dprd2d2  19943  eldm3  35736  dfdm5  35748  dfrn5  35749  elfuns  35891  dfiota3  35899  brimg  35913  funpartlem  35918  bj-19.12  36737  bj-nnflemee  36739  bj-restuni  37073  sbccom2lem  38106  dmqsblocks  38833  diblsmopel  41153  dicelval3  41162  dihjatcclem4  41403  19.9dev  42190  nnoeomeqom  43288  pm11.6  44368  ax6e2ndeq  44536  e2ebind  44540  ax6e2ndeqVD  44885  e2ebindVD  44888  e2ebindALT  44905  ax6e2ndeqALT  44907  ich2ex  47456  ichexmpl1  47457  elsprel  47463  eliunxp2  48322