Theorem excom 1642

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

Syntax hints:   ↔ wb 104  ∃wex 1468

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-4 1487  ax-ial 1514

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  excom13  1667  exrot3  1668  ee4anv  1904  sbexyz  1976  2exsb  1982  2euex  2084  2exeu  2089  2eu4  2090  rexcomf  2591  gencbvex  2727  euxfr2dc  2864  euind  2866  sbccomlem  2978  opelopabsbALT  4176  uniuni  4367  elvvv  4597  elco  4700  dmuni  4744  dm0rn0  4751  dmmrnm  4753  dmcosseq  4805  elres  4850  rnco  5040  coass  5052  oprabid  5796  dfoprab2  5811  opabex3d  6012  opabex3  6013  cnvoprab  6124  domen  6638  xpassen  6717  prarloc  7304  fisumcom2  11200