Theorem excom 1657

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 1656	. 2 ⊢ (∃𝑥∃𝑦𝜑 → ∃𝑦∃𝑥𝜑)
2		excomim 1656	. 2 ⊢ (∃𝑦∃𝑥𝜑 → ∃𝑥∃𝑦𝜑)
3	1, 2	impbii 125	1 ⊢ (∃𝑥∃𝑦𝜑 ↔ ∃𝑦∃𝑥𝜑)

Syntax hints:   ↔ wb 104  ∃wex 1485

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 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-4 1503  ax-ial 1527

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  excom13  1682  exrot3  1683  ee4anv  1927  sbexyz  1996  2exsb  2002  2euex  2106  2exeu  2111  2eu4  2112  rexcomf  2632  gencbvex  2776  euxfr2dc  2915  euind  2917  sbccomlem  3029  opelopabsbALT  4244  uniuni  4436  elvvv  4674  elco  4777  dmuni  4821  dm0rn0  4828  dmmrnm  4830  dmcosseq  4882  elres  4927  rnco  5117  coass  5129  oprabid  5885  dfoprab2  5900  opabex3d  6100  opabex3  6101  cnvoprab  6213  domen  6729  xpassen  6808  prarloc  7465  fisumcom2  11401  fprodcom2fi  11589