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  2785  euxfr2dc  2924  euind  2926  sbccomlem  3039  opelopabsbALT  4261  uniuni  4453  elvvv  4691  elco  4795  dmuni  4839  dm0rn0  4846  dmmrnm  4848  dmcosseq  4900  elres  4945  rnco  5137  coass  5149  oprabid  5909  dfoprab2  5924  opabex3d  6124  opabex3  6125  cnvoprab  6237  domen  6753  xpassen  6832  prarloc  7504  fisumcom2  11448  fprodcom2fi  11636