Theorem excom 1042

Description: Theorem 19.11 of [Margaris] p. 89.

Assertion

Ref	Expression
excom	|- (E.xE.yph <-> E.yE.xph)

Proof of Theorem excom

Step	Hyp	Ref	Expression
1		excomim 1041	. 2 |- (E.xE.yph -> E.yE.xph)
2		excomim 1041	. 2 |- (E.yE.xph -> E.xE.yph)
3	1, 2	impbi 157	1 |- (E.xE.yph <-> E.yE.xph)

Syntax hints:   <-> wb 146  E.wex 977

This theorem is referenced by:  excom13 1094  exrot3 1095  ee4anv 1320  2exsb 1346  2euex 1434  2exeu 1439  2eu1 1442  2eu4 1445  rexcom 1767  gencbvex 1829  sbccomglem 1978  dfiun2g 2576  iunn0 2597  opabid 2799  uniuni 2870  dmuni 3308  dm0rn0 3319  dmcoss 3347  dmcosseq 3349  rnuni 3445  rnco 3488  coass 3498  imaiun 3849  iinon 3895  dfoprab2 3976  2nd2val 4080  2ndconst 4081  domen 4361  xpcomen 4419  xpassen 4421  scott0 4689  aceq5lem1 4707  aceq5lem4 4710  cflem 4877  genpass 5084  addcompr 5095  mulcompr 5097  ltexprlem1 5114  ltexprlem4 5117  reclem1pr 5128  reclem2pr 5129  suplem1pr 5133

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 959  ax-gen 960  ax-4 970  ax-5o 972  ax-6o 975

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 978

Copyright terms: Public domain