Theorem excom 1712

Description: Theorem 19.11 of [Margaris] p. 89. (Contributed by NM, 5-Aug-1993.)

Assertion

Ref	Expression
excom	|- ( E. x E. y ph <-> E. y E. x ph )

Proof of Theorem excom

Step	Hyp	Ref	Expression
1		excomim 1711	. 2 |- ( E. x E. y ph -> E. y E. x ph )
2		excomim 1711	. 2 |- ( E. y E. x ph -> E. x E. y ph )
3	1, 2	impbii 126	1 |- ( E. x E. y ph <-> E. y E. x ph )

Syntax hints:   <-> wb 105   E.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  1988  sbexyz  2057  2exsb  2063  2euex  2168  2exeu  2173  2eu4  2174  rexcomf  2705  gencbvex  2861  euxfr2dc  3002  euind  3004  sbccomlem  3117  opelopabsbALT  4377  uniuni  4572  elvvv  4813  elco  4921  dmuni  4966  dm0rn0  4973  dmmrnm  4976  dmcosseq  5029  elres  5074  rnco  5269  coass  5281  oprabid  6082  dfoprab2  6100  opabex3d  6314  opabex3  6315  cnvoprab  6430  domen  6988  xpassen  7081  prarloc  7818  fisumcom2  12124  fprodcom2fi  12312