Theorem breqtrrd 2641

Description: Substitution of equal classes into a binary relation.

Hypotheses

Ref	Expression
breqtrrd.1	|- (ph -> ARB)
breqtrrd.2	|- (ph -> C = B)

Assertion

Ref	Expression
breqtrrd	|- (ph -> ARC)

Proof of Theorem breqtrrd

Step	Hyp	Ref	Expression
1		breqtrrd.1	. 2 |- (ph -> ARB)
2		breqtrrd.2	. . 3 |- (ph -> C = B)
3	2	eqcomd 1480	. 2 |- (ph -> B = C)
4	1, 3	breqtrd 2639	1 |- (ph -> ARC)

Syntax hints:   -> wi 3   = wceq 956   class class class wbr 2619

This theorem is referenced by:  addgtge0t 5649  xrmax1 5909  xrmax2 5910  max1ALT 5916  flhalft 6246  ser1mono 6337  expmwordit 6606  sqgt0t 6622  expnbndt 6654  facwordit 6944  faclbnd5 6953  faclbnd6 6954  fsumcmp 7040  fsumcmpndx2 7042  fsumabs 7043  cvgcmp2lem 7180  cvgcmp2clem 7182  cvgcmp3c 7186  isumclim2tf 7198  iserzgt0 7211  infcvglem3 7223  cvgratlem1 7250  cvgratlem5 7254  efcltlem1 7304  efcvg 7314  erelem3 7321  ef1tllem 7381  eirrlem4 7392  effsumle 7397  sin01bndlem2 7468  sin01bndlem3 7469  cos01bndlem2 7470  cos01bndlem3 7471  sin02gt0 7478  ruclem26 7535  ruclem28 7537  mettri 7817  mettri3 7818  metxplem4 7833  bl2in 7843  lmnn 7935  nvabs 8301  sqcn 8335  nmoge0 8430  nmolb 8434  siii 8513  minveclem16 8560  minveclem31 8575  hlipgt0 8616  sinq12gt0t 8708  normge0t 8992  normpyct 9013  pjige0 9635  nmoplbt 9831  nmfnlbt 9848  branmfnt 10038  hmopidmch 10079  pjssdif2 10102  stle 10167  strlem3a 10179  truni1 10499  mslb1 10629

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-8 964  ax-10 966  ax-12 968  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-10o 1140  ax-16 1210  ax-11o 1218  ax-ext 1459

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 981  df-sb 1172  df-clab 1464  df-cleq 1469  df-clel 1472  df-v 1812  df-un 2050  df-sn 2412  df-pr 2413  df-op 2416  df-br 2620

Copyright terms: Public domain