Theorem excom 2162

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 2007, ax-10 2141, ax-12 2177. (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 2159	. . 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 2157

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

This theorem is referenced by:  excomim  2163  excom13  2164  exrot3  2165  eeor  2335  ee4anv  2353  ee4anvOLD  2354  2sb8ef  2359  sbel2x  2479  2sb8e  2535  2euexv  2631  2euex  2641  2eu4  2655  rexcom4  3288  rexcomf  3303  gencbvex  3541  euind  3730  sbccomlemOLD  3870  elvvv  5761  dmuni  5925  dm0rn0  5935  dmcosseqOLD  5988  cnvopab  6157  rnco  6272  coass  6285  oprabidw  7462  oprabid  7463  dfoprab2  7491  uniuni  7782  opabex3d  7990  opabex3rd  7991  opabex3  7992  frxp  8151  domen  9002  xpassen  9106  scott0  9926  dfac5lem1  10163  dfac5lem4OLD  10168  cflemOLD  10286  ltexprlem1  11076  ltexprlem4  11079  fsumcom2  15810  fprodcom2  16020  gsumval3eu  19922  dprd2d2  20064  eldm3  35761  dfdm5  35773  dfrn5  35774  elfuns  35916  dfiota3  35924  brimg  35938  funpartlem  35943  bj-19.12  36762  bj-nnflemee  36764  bj-restuni  37098  sbccom2lem  38131  diblsmopel  41173  dicelval3  41182  dihjatcclem4  41423  19.9dev  42253  nnoeomeqom  43325  pm11.6  44411  ax6e2ndeq  44579  e2ebind  44583  ax6e2ndeqVD  44929  e2ebindVD  44932  e2ebindALT  44949  ax6e2ndeqALT  44951  ich2ex  47455  ichexmpl1  47456  elsprel  47462  eliunxp2  48250