Theorem excom 1688

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

Syntax hints:   ↔ wb 105  ∃wex 1516

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 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-4 1534  ax-ial 1558

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  excom13  1713  exrot3  1714  ee4anv  1963  sbexyz  2032  2exsb  2038  2euex  2142  2exeu  2147  2eu4  2148  rexcomf  2669  gencbvex  2821  euxfr2dc  2962  euind  2964  sbccomlem  3077  opelopabsbALT  4313  uniuni  4506  elvvv  4746  elco  4852  dmuni  4897  dm0rn0  4904  dmmrnm  4906  dmcosseq  4959  elres  5004  rnco  5198  coass  5210  oprabid  5989  dfoprab2  6005  opabex3d  6219  opabex3  6220  cnvoprab  6333  domen  6853  xpassen  6940  prarloc  7636  fisumcom2  11824  fprodcom2fi  12012