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  1990  sbexyz  2059  2exsb  2065  2euex  2170  2exeu  2175  2eu4  2176  rexcomf  2707  gencbvex  2863  euxfr2dc  3005  euind  3007  sbccomlem  3120  opelopabsbALT  4382  uniuni  4577  elvvv  4818  elco  4926  dmuni  4971  dm0rn0  4978  dmmrnm  4981  dmcosseq  5034  elres  5079  rnco  5274  coass  5286  oprabid  6090  dfoprab2  6108  opabex3d  6323  opabex3  6324  cnvoprab  6443  domen  7001  xpassen  7094  prarloc  7834  fisumcom2  12149  fprodcom2fi  12337