Theorem eqbrtrd 3895

Description: Substitution of equal classes into a binary relation. (Contributed by NM, 8-Oct-1999.)

Hypotheses

Ref	Expression
eqbrtrd.1	⊢ (𝜑 → 𝐴 = 𝐵)
eqbrtrd.2	⊢ (𝜑 → 𝐵𝑅𝐶)

Assertion

Ref	Expression
eqbrtrd	⊢ (𝜑 → 𝐴𝑅𝐶)

Proof of Theorem eqbrtrd

Step	Hyp	Ref	Expression
1		eqbrtrd.2	. 2 ⊢ (𝜑 → 𝐵𝑅𝐶)
2		eqbrtrd.1	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
3	2	breq1d 3885	. 2 ⊢ (𝜑 → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐶))
4	1, 3	mpbird 166	1 ⊢ (𝜑 → 𝐴𝑅𝐶)

Syntax hints:   → wi 4   = wceq 1299   class class class wbr 3875

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 671  ax-5 1391  ax-7 1392  ax-gen 1393  ax-ie1 1437  ax-ie2 1438  ax-8 1450  ax-10 1451  ax-11 1452  ax-i12 1453  ax-bndl 1454  ax-4 1455  ax-17 1474  ax-i9 1478  ax-ial 1482  ax-i5r 1483  ax-ext 2082

This theorem depends on definitions:  df-bi 116  df-3an 932  df-tru 1302  df-nf 1405  df-sb 1704  df-clab 2087  df-cleq 2093  df-clel 2096  df-nfc 2229  df-v 2643  df-un 3025  df-sn 3480  df-pr 3481  df-op 3483  df-br 3876

This theorem is referenced by:  eqbrtrrd  3897  dif1en  6702  prarloclemcalc  7211  ltexprlemopu  7312  recexprlemloc  7340  caucvgprprlemloccalc  7393  mulle0r  8560  lbinfle  8566  divge1  9357  xltnegi  9459  xleadd1a  9497  xltadd1  9500  xlt2add  9504  xposdif  9506  xleaddadd  9511  ubmelm1fzo  9844  qbtwnrelemcalc  9874  qbtwnxr  9876  ceiqm1l  9925  ceilqm1lt  9926  ceilqle  9928  modqlt  9947  modqeqmodmin  10008  addmodlteq  10012  exp3vallem  10135  bernneq  10253  faclbnd2  10329  resqrexlemdec  10623  resqrexlemcalc2  10627  resqrexlemglsq  10634  resqrexlemga  10635  abslt  10700  amgm2  10730  icodiamlt  10792  maxabsle  10816  maxltsup  10830  minmax  10840  min1inf  10842  min2inf  10843  bdtrilem  10849  xrmaxltsup  10866  xrmaxaddlem  10868  xrmaxadd  10869  xrminmax  10873  xrmin1inf  10875  xrmin2inf  10876  climconst  10898  serclim0  10913  mulcn2  10920  reccn2ap  10921  iserex  10947  climlec2  10949  iserge0  10951  climcau  10955  climcvg1nlem  10957  fsumabs  11073  iserabs  11083  isumlessdc  11104  divcnv  11105  expcnvre  11111  absgtap  11118  georeclim  11121  cvgratnnlembern  11131  cvgratnnlemsumlt  11136  cvgratnnlemfm  11137  cvgratnnlemrate  11138  mertenslemub  11142  mertenslemi1  11143  efcvgfsum  11171  eftlub  11194  eflegeo  11206  tanval3ap  11219  tannegap  11233  ef01bndlem  11261  sin01bnd  11262  cos01bnd  11263  cos01gt0  11267  mulgcd  11497  eucalglt  11531  lcmledvds  11544  mulgcddvds  11568  prmind2  11594  pw2dvdslemn  11635  pw2dvdseulemle  11637  oddpwdclemdvds  11640  sqrt2irrap  11650  divdenle  11667  nonsq  11677  ennnfonelemkh  11717  bl2in  12331  xblcntrps  12341  xblcntr  12342  ssblps  12353  ssbl  12354  blssps  12355  blss  12356  mulc1cncf  12489  cncfmptc  12495  mulcncflem  12502  limcimolemlt  12513  qdencn  12806  cvgcmp2nlemabs  12811  trilpolemclim  12813  trilpolemisumle  12815  trilpolemeq1  12817