Theorem excom 1675

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

Syntax hints:   ↔ wb 105  ∃wex 1503

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 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-4 1521  ax-ial 1545

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  excom13  1700  exrot3  1701  ee4anv  1950  sbexyz  2019  2exsb  2025  2euex  2129  2exeu  2134  2eu4  2135  rexcomf  2656  gencbvex  2807  euxfr2dc  2946  euind  2948  sbccomlem  3061  opelopabsbALT  4290  uniuni  4483  elvvv  4723  elco  4829  dmuni  4873  dm0rn0  4880  dmmrnm  4882  dmcosseq  4934  elres  4979  rnco  5173  coass  5185  oprabid  5951  dfoprab2  5966  opabex3d  6175  opabex3  6176  cnvoprab  6289  domen  6807  xpassen  6886  prarloc  7565  fisumcom2  11584  fprodcom2fi  11772