Theorem breqtrrd 2646

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 1483	. 2 |- (ph -> B = C)
4	1, 3	breqtrd 2644	1 |- (ph -> ARC)

Syntax hints:   -> wi 3   = wceq 958   class class class wbr 2624

This theorem is referenced by:  addgtge0t 5661  xrmax1 5911  xrmax2 5912  max1ALT 5918  flhalft 6248  ser1mono 6338  expmwordit 6607  sqgt0t 6623  expnbndt 6655  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 7469  sin01bndlem3 7470  cos01bndlem2 7471  cos01bndlem3 7472  sin02gt0 7479  ruclem26 7536  ruclem28 7538  mettri 7814  mettri3 7815  metxplem4 7830  bl2in 7840  lmnn 7932  nvabs 8297  sqcn 8331  nmoge0 8426  nmolb 8430  siii 8509  minveclem16 8556  minveclem31 8571  hlipgt0 8612  sinq12gt0t 8703  normge0t 8987  normpyct 9008  pjige0 9630  nmoplbt 9826  nmfnlbt 9843  branmfnt 10033  hmopidmch 10074  pjssdif2 10097  stle 10162  strlem3a 10174  truni1 10485  mslb1 10600

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 964  ax-gen 965  ax-8 966  ax-10 968  ax-12 970  ax-17 973  ax-4 975  ax-5o 977  ax-6o 980  ax-9o 1125  ax-10o 1142  ax-16 1212  ax-11o 1220  ax-ext 1462

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 983  df-sb 1174  df-clab 1467  df-cleq 1472  df-clel 1475  df-v 1815  df-un 2053  df-sn 2416  df-pr 2417  df-op 2420  df-br 2625

Copyright terms: Public domain