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 ⊢ (∃𝑥∃𝑦𝜑 ↔ ∃𝑦∃𝑥𝜑)

This proof depends on syntax axioms:   ↔ wb 105  ∃wex 1545

This proof depends on 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 proof depends on definitions:  df-bi 117

This theorem is used 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  4401  uniuni  4597  elvvv  4838  elco  4946  dmuni  4991  dm0rn0  4998  dmmrnm  5001  dmcosseq  5054  elres  5099  rnco  5294  coass  5306  oprabid  6117  dfoprab2  6135  opabex3d  6350  opabex3  6351  cnvoprab  6470  domen  7035  xpassen  7128  prarloc  7870  fisumcom2  12205  fprodcom2fi  12393