Theorem excom 1688

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 1687	. 2 |- ( E. x E. y ph -> E. y E. x ph )
2		excomim 1687	. 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 1516

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 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-4 1534  ax-ial 1558

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  excom13  1713  exrot3  1714  ee4anv  1963  sbexyz  2032  2exsb  2038  2euex  2143  2exeu  2148  2eu4  2149  rexcomf  2670  gencbvex  2824  euxfr2dc  2965  euind  2967  sbccomlem  3080  opelopabsbALT  4323  uniuni  4516  elvvv  4756  elco  4862  dmuni  4907  dm0rn0  4914  dmmrnm  4916  dmcosseq  4969  elres  5014  rnco  5208  coass  5220  oprabid  5999  dfoprab2  6015  opabex3d  6229  opabex3  6230  cnvoprab  6343  domen  6863  xpassen  6950  prarloc  7651  fisumcom2  11864  fprodcom2fi  12052