Theorem excom 1712

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

Syntax hints:   ↔ wb 105  ∃wex 1541

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 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-ial 1583

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  excom13  1737  exrot3  1738  ee4anv  1987  sbexyz  2056  2exsb  2062  2euex  2167  2exeu  2172  2eu4  2173  rexcomf  2696  gencbvex  2851  euxfr2dc  2992  euind  2994  sbccomlem  3107  opelopabsbALT  4359  uniuni  4554  elvvv  4795  elco  4902  dmuni  4947  dm0rn0  4954  dmmrnm  4957  dmcosseq  5010  elres  5055  rnco  5250  coass  5262  oprabid  6060  dfoprab2  6078  opabex3d  6292  opabex3  6293  cnvoprab  6408  domen  6965  xpassen  7057  prarloc  7766  fisumcom2  12062  fprodcom2fi  12250