Theorem excom 1678

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

Syntax hints:   ↔ wb 105  ∃wex 1506

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 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-4 1524  ax-ial 1548

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  excom13  1703  exrot3  1704  ee4anv  1953  sbexyz  2022  2exsb  2028  2euex  2132  2exeu  2137  2eu4  2138  rexcomf  2659  gencbvex  2810  euxfr2dc  2949  euind  2951  sbccomlem  3064  opelopabsbALT  4294  uniuni  4487  elvvv  4727  elco  4833  dmuni  4877  dm0rn0  4884  dmmrnm  4886  dmcosseq  4938  elres  4983  rnco  5177  coass  5189  oprabid  5957  dfoprab2  5973  opabex3d  6187  opabex3  6188  cnvoprab  6301  domen  6819  xpassen  6898  prarloc  7587  fisumcom2  11620  fprodcom2fi  11808