Theorem excom 1044

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 1043	. 2 |- (E.xE.yph -> E.yE.xph)
2		excomim 1043	. 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 978

This theorem is referenced by:  excom13 1096  exrot3 1097  ee4anv 1323  2exsb 1349  2euex 1439  2exeu 1444  2eu1 1447  2eu4 1450  rexcom 1772  gencbvex 1834  sbccomglem 1984  dfiun2g 2581  iunn0 2602  opabid 2805  uniuni 2875  dmuni 3314  dm0rn0 3325  dmcoss 3355  dmcosseq 3357  rnuni 3451  rnco 3494  coass 3504  imaiun 3855  iinon 3901  dfoprab2 3982  2nd2val 4086  2ndconst 4087  domen 4367  xpcomen 4425  xpassen 4427  scott0 4697  aceq5lem1 4715  aceq5lem4 4718  cflem 4885  genpass 5092  addcompr 5103  mulcompr 5105  ltexprlem1 5122  ltexprlem4 5125  reclem1pr 5136  reclem2pr 5137  suplem1pr 5141

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-4 971  ax-5o 973  ax-6o 976

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

Copyright terms: Public domain