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  2671  gencbvex  2825  euxfr2dc  2966  euind  2968  sbccomlem  3081  opelopabsbALT  4324  uniuni  4517  elvvv  4757  elco  4863  dmuni  4908  dm0rn0  4915  dmmrnm  4917  dmcosseq  4970  elres  5015  rnco  5209  coass  5221  oprabid  6001  dfoprab2  6017  opabex3d  6231  opabex3  6232  cnvoprab  6345  domen  6865  xpassen  6952  prarloc  7653  fisumcom2  11910  fprodcom2fi  12098