Theorem eqbrtrd 2625

Description: Substitution of equal classes into a binary relation.

Hypotheses

Ref	Expression
eqbrtrd.1	|- (ph -> A = B)
eqbrtrd.2	|- (ph -> BRC)

Assertion

Ref	Expression
eqbrtrd	|- (ph -> ARC)

Proof of Theorem eqbrtrd

Step	Hyp	Ref	Expression
1		eqbrtrd.2	. 2 |- (ph -> BRC)
2		eqbrtrd.1	. . 3 |- (ph -> A = B)
3	2	breq1d 2619	. 2 |- (ph -> (ARC <-> BRC))
4	1, 3	mpbird 196	1 |- (ph -> ARC)

Syntax hints:   -> wi 3   = wceq 953   class class class wbr 2609

This theorem is referenced by:  eqbrtrrd 2627  cdafi 4908  xrmin1 5859  xrmin2 5860  lbinfmle 5997  ceim1lt 6192  bernneq 6583  caure 6864  cauim 6865  faclbnd2 6883  faclbnd4lem3 6887  fsumcmp 6978  fsumabs2mul 6982  serzclim0 7046  climrecl 7047  climaddlem3 7052  climmullem4 7059  climmullem5 7060  climabslem 7084  climcau 7092  ser1cmp0 7111  cvgcmp3c 7122  cvgcmp3cetlem1 7124  reccnv 7153  georeclim 7175  geoisumr 7178  cvgratlem5 7189  mulc1cncf 7214  efaddlem10 7289  efaddlem11 7290  efaddlem16 7295  efaddlem17 7296  sin01bndlem3 7411  cos01bndlem3 7413  cos01gt0 7419  ruclem27 7479  alephsuc3 7527  metxplem4 7773  blcntr 7785  dscmet 7856  lmconst 7872  metcnp4lem2 7903  bcthlem20 7952  bcthlem21 7953  nvmtri2 8239  nvabs 8240  nvge0 8241  nvlmle 8268  sm1cnilem 8281  nmoubi 8367  nmblolbii 8390  blocnilem 8395  siii 8444  ubthlem3 8462  ubthlem10 8469  minveclem14 8489  minveclem21 8496  minveclem38 8513  htthlem6 8555  htthlem10 8559  bcsALT 8967  bcs3t 8971  projlem26 9127  nmopubt 9749  nmfnleubt 9765  nmbdoplb 9864  nmcoplb 9873  nmophm 9876  nmbdfnlb 9893  nmcfnlb 9902  nlelch 9909  riesz1t 9913  cnlnadjlem2 9916  nmopadjle 9936  nmoptri 9941  nmopco 9942  nmopcoadj 9948  unierr 9950  branmfnt 9951  hmopidmchlem 9989  pjs14 10048  hstlet 10067  strlem3a 10089  cdj3lem2b 10269  mslb1 10473  msra3 10475

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-8 961  ax-10 963  ax-12 965  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975  ax-9o 1119  ax-10o 1136  ax-16 1206  ax-11o 1213  ax-ext 1452

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 978  df-sb 1168  df-clab 1457  df-cleq 1462  df-clel 1465  df-v 1803  df-un 2040  df-sn 2402  df-pr 2403  df-op 2406  df-br 2610

Copyright terms: Public domain