Theorem excom 1643

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

Syntax hints:   ↔ wb 104  ∃wex 1469

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 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-4 1488  ax-ial 1515

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  excom13  1668  exrot3  1669  ee4anv  1907  sbexyz  1979  2exsb  1985  2euex  2087  2exeu  2092  2eu4  2093  rexcomf  2596  gencbvex  2735  euxfr2dc  2873  euind  2875  sbccomlem  2987  opelopabsbALT  4189  uniuni  4380  elvvv  4610  elco  4713  dmuni  4757  dm0rn0  4764  dmmrnm  4766  dmcosseq  4818  elres  4863  rnco  5053  coass  5065  oprabid  5811  dfoprab2  5826  opabex3d  6027  opabex3  6028  cnvoprab  6139  domen  6653  xpassen  6732  prarloc  7335  fisumcom2  11239