Theorem excom 1716

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

Syntax hints:   ↔ wb 105  ∃wex 1545

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 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-ial 1587

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  excom13  1741  exrot3  1742  ee4anv  1994  sbexyz  2063  2exsb  2069  2euex  2174  2exeu  2179  2eu4  2180  rexcomf  2713  gencbvex  2869  euxfr2dc  3011  euind  3013  sbccomlem  3126  opelopabsbALT  4396  uniuni  4592  elvvv  4833  elco  4941  dmuni  4986  dm0rn0  4993  dmmrnm  4996  dmcosseq  5049  elres  5094  rnco  5289  coass  5301  oprabid  6107  dfoprab2  6125  opabex3d  6340  opabex3  6341  cnvoprab  6460  domen  7025  xpassen  7118  prarloc  7860  fisumcom2  12183  fprodcom2fi  12371