Theorem excom 1664

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

Syntax hints:   ↔ wb 105  ∃wex 1492

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510  ax-ial 1534

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  excom13  1689  exrot3  1690  ee4anv  1934  sbexyz  2003  2exsb  2009  2euex  2113  2exeu  2118  2eu4  2119  rexcomf  2639  gencbvex  2783  euxfr2dc  2922  euind  2924  sbccomlem  3037  opelopabsbALT  4259  uniuni  4451  elvvv  4689  elco  4793  dmuni  4837  dm0rn0  4844  dmmrnm  4846  dmcosseq  4898  elres  4943  rnco  5135  coass  5147  oprabid  5906  dfoprab2  5921  opabex3d  6121  opabex3  6122  cnvoprab  6234  domen  6750  xpassen  6829  prarloc  7501  fisumcom2  11441  fprodcom2fi  11629