Theorem excom 1652

Description: Theorem 19.11 of [Margaris] p. 89. (Contributed by NM, 5-Aug-1993.)

Assertion

Ref	Expression
excom	⊢ (∃𝑥∃𝑦𝜑 ↔ ∃𝑦∃𝑥𝜑)

Proof of Theorem excom

Step	Hyp	Ref	Expression
1		excomim 1651	. 2 ⊢ (∃𝑥∃𝑦𝜑 → ∃𝑦∃𝑥𝜑)
2		excomim 1651	. 2 ⊢ (∃𝑦∃𝑥𝜑 → ∃𝑥∃𝑦𝜑)
3	1, 2	impbii 125	1 ⊢ (∃𝑥∃𝑦𝜑 ↔ ∃𝑦∃𝑥𝜑)

Syntax hints:   ↔ wb 104  ∃wex 1480

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1435  ax-7 1436  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-4 1498  ax-ial 1522

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  excom13  1677  exrot3  1678  ee4anv  1922  sbexyz  1991  2exsb  1997  2euex  2101  2exeu  2106  2eu4  2107  rexcomf  2628  gencbvex  2772  euxfr2dc  2911  euind  2913  sbccomlem  3025  opelopabsbALT  4237  uniuni  4429  elvvv  4667  elco  4770  dmuni  4814  dm0rn0  4821  dmmrnm  4823  dmcosseq  4875  elres  4920  rnco  5110  coass  5122  oprabid  5874  dfoprab2  5889  opabex3d  6089  opabex3  6090  cnvoprab  6202  domen  6717  xpassen  6796  prarloc  7444  fisumcom2  11379  fprodcom2fi  11567