Theorem excom 1675

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

Syntax hints:   ↔ wb 105  ∃wex 1503

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 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-4 1521  ax-ial 1545

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  excom13  1700  exrot3  1701  ee4anv  1950  sbexyz  2019  2exsb  2025  2euex  2129  2exeu  2134  2eu4  2135  rexcomf  2656  gencbvex  2806  euxfr2dc  2945  euind  2947  sbccomlem  3060  opelopabsbALT  4289  uniuni  4482  elvvv  4722  elco  4828  dmuni  4872  dm0rn0  4879  dmmrnm  4881  dmcosseq  4933  elres  4978  rnco  5172  coass  5184  oprabid  5950  dfoprab2  5965  opabex3d  6173  opabex3  6174  cnvoprab  6287  domen  6805  xpassen  6884  prarloc  7563  fisumcom2  11581  fprodcom2fi  11769