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  4383  uniuni  4579  elvvv  4820  elco  4928  dmuni  4973  dm0rn0  4980  dmmrnm  4983  dmcosseq  5036  elres  5081  rnco  5276  coass  5288  oprabid  6092  dfoprab2  6110  opabex3d  6325  opabex3  6326  cnvoprab  6445  domen  7003  xpassen  7096  prarloc  7836  fisumcom2  12155  fprodcom2fi  12343