Theorem excom 1716

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

This proof depends on syntax axioms:   <-> wb 105   E.wex 1545

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-4 1563  ax-ial 1587

This proof depends on definitions:  df-bi 117

This theorem is used by:  excom13  1741  exrot3  1742  ee4anv  1994  sbexyz  2063  2exsb  2069  2euex  2174  2exeu  2179  2eu4  2180  rexcomf  2713  gencbvex  2869  euxfr2dc  3011  euind  3013  sbccomlem  3126  opelopabsbALT  4403  uniuni  4599  elvvv  4840  elco  4948  dmuni  4993  dm0rn0  5000  dmmrnm  5003  dmcosseq  5056  elres  5101  rnco  5297  coass  5309  oprabid  6120  dfoprab2  6138  opabex3d  6354  opabex3  6355  cnvoprab  6474  domen  7039  xpassen  7132  prarloc  7876  fisumcom2  12230  fprodcom2fi  12418