Theorem excom 2197

Description: Theorem 19.11 of [Margaris] p. 89. (Contributed by NM, 5-Aug-1993.) Remove dependencies on ax-5 1940, ax-6 1997, ax-7 2038, ax-10 2176, ax-12 2213. (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 2194	. . 3 ⊢ (∀𝑥∀𝑦 ¬ 𝜑 ↔ ∀𝑦∀𝑥 ¬ 𝜑)
2	1	notbii 323	. 2 ⊢ (¬ ∀𝑥∀𝑦 ¬ 𝜑 ↔ ¬ ∀𝑦∀𝑥 ¬ 𝜑)
3		2exnaln 1859	. 2 ⊢ (∃𝑥∃𝑦𝜑 ↔ ¬ ∀𝑥∀𝑦 ¬ 𝜑)
4		2exnaln 1859	. 2 ⊢ (∃𝑦∃𝑥𝜑 ↔ ¬ ∀𝑦∀𝑥 ¬ 𝜑)
5	2, 3, 4	3bitr4i 306	1 ⊢ (∃𝑥∃𝑦𝜑 ↔ ∃𝑦∃𝑥𝜑)

Syntax hints:  ¬ wn 3   ↔ wb 209  ∀wal 1568  ∃wex 1809

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-11 2192

This theorem depends on definitions:  df-bi 210  df-ex 1810

This theorem is referenced by:  excomim  2198  excom13  2199  exrot3  2200  eeor  2366  ee4anv  2383  ee4anvOLD  2384  2sb8ef  2388  sbel2x  2506  2sb8e  2562  2euexv  2659  2euex  2669  2eu4  2682  rexcom4  3292  rexcomf  3304  gencbvex  3511  euind  3688  sbccomlemOLD  3824  elvvv  5739  dmuni  5906  dm0rn0OLD  5917  cnvopab  6139  rncoOLD  6256  coass  6269  oprabidw  7443  oprabid  7444  dfoprab2  7470  uniuni  7762  opabex3d  7963  opabex3rd  7964  opabex3  7965  frxp  8123  domen  8959  xpassen  9060  scott0  9861  dfac5lem1  10108  cflemOLD  10230  ltexprlem1  11022  ltexprlem4  11025  fsumcom2  15827  fprodcom2  16040  gsumval3eu  19975  dprd2d2  20117  eldm3  36234  dfdm5  36246  dfrn5  36247  elfuns  36386  dfiota3  36394  brimg  36408  funpartlem  36415  bj-19.12  37329  bj-nnflemee  37393  bj-restuni  37720  sbccom2lem  38754  dmqsblocks  39597  diblsmopel  41926  dicelval3  41935  dihjatcclem4  42176  nfe2  42965  19.9dev  42967  nnoeomeqom  44022  pm11.6  45085  ax6e2ndeq  45251  e2ebind  45255  ax6e2ndeqVD  45600  e2ebindVD  45603  e2ebindALT  45620  ax6e2ndeqALT  45622  ich2ex  48200  ichexmpl1  48201  elsprel  48207  eliunxp2  49097