Theorem excom 1644

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

Syntax hints:   ↔ wb 104  ∃wex 1472

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 1427  ax-7 1428  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-4 1490  ax-ial 1514

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  excom13  1669  exrot3  1670  ee4anv  1914  sbexyz  1983  2exsb  1989  2euex  2093  2exeu  2098  2eu4  2099  rexcomf  2619  gencbvex  2758  euxfr2dc  2897  euind  2899  sbccomlem  3011  opelopabsbALT  4219  uniuni  4411  elvvv  4649  elco  4752  dmuni  4796  dm0rn0  4803  dmmrnm  4805  dmcosseq  4857  elres  4902  rnco  5092  coass  5104  oprabid  5853  dfoprab2  5868  opabex3d  6069  opabex3  6070  cnvoprab  6181  domen  6696  xpassen  6775  prarloc  7423  fisumcom2  11335  fprodcom2fi  11523