Theorem eqbrtrd 4131

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 4119	. 2 ⊢ (𝜑 → (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐶))
4	1, 3	mpbird 167	1 ⊢ (𝜑 → 𝐴𝑅𝐶)

Syntax hints:   → wi 4   = wceq 1398   class class class wbr 4109

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2214

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-v 2815  df-un 3215  df-sn 3695  df-pr 3696  df-op 3698  df-br 4110

This theorem is referenced by:  eqbrtrrd  4133  dif1en  7136  ccfunen  7578  prarloclemcalc  7817  ltexprlemopu  7918  recexprlemloc  7946  caucvgprprlemloccalc  7999  suplocsrlem  8123  axpre-suploclemres  8216  mulle0r  9218  lbinfle  9224  divge1  10056  xltnegi  10168  xleadd1a  10206  xltadd1  10209  xlt2add  10213  xposdif  10215  xleaddadd  10220  lincmble  10337  ubmelm1fzo  10571  zsupssdc  10598  qbtwnrelemcalc  10615  qbtwnxr  10617  ceiqm1l  10673  ceilqm1lt  10674  ceilqle  10676  modqlt  10695  modqeqmodmin  10756  addmodlteq  10760  seqf1oglem1  10881  exp3vallem  10902  bernneq  11022  nn0ltexp2  11071  faclbnd2  11104  sshashneg  11205  ccatsymb  11290  ccatrn  11297  resqrexlemdec  11696  resqrexlemcalc2  11700  resqrexlemglsq  11707  resqrexlemga  11708  abslt  11773  amgm2  11803  icodiamlt  11865  maxabsle  11889  maxltsup  11903  minmax  11915  min1inf  11917  min2inf  11918  bdtrilem  11924  xrmaxltsup  11943  xrmaxaddlem  11945  xrmaxadd  11946  xrminmax  11950  xrmin1inf  11952  xrmin2inf  11953  climconst  11975  serclim0  11990  mulcn2  11997  reccn2ap  11998  iserex  12024  climlec2  12026  iserge0  12028  climcau  12032  climcvg1nlem  12034  fsumabs  12151  iserabs  12161  isumlessdc  12182  divcnv  12183  expcnvre  12189  absgtap  12196  georeclim  12199  cvgratnnlembern  12209  cvgratnnlemsumlt  12214  cvgratnnlemfm  12215  cvgratnnlemrate  12216  mertenslemub  12220  mertenslemi1  12221  prodfclim1  12230  prodfap0  12231  efcvgfsum  12353  eftlub  12376  eflegeo  12387  tanval3ap  12400  tannegap  12414  ef01bndlem  12442  sin01bnd  12443  cos01bnd  12444  cos01gt0  12449  bitsfzolem  12640  bitsfzo  12641  bitsinv1lem  12647  mulgcd  12712  nnminle  12731  eucalglt  12754  lcmledvds  12767  mulgcddvds  12791  prmind2  12817  isprm5lem  12838  pw2dvdslemn  12862  pw2dvdseulemle  12864  oddpwdclemdvds  12867  sqrt2irrap  12877  divdenle  12894  nonsq  12904  pythagtriplem4  12966  pclem0  12984  pcpremul  12991  pczdvds  13012  pcprmpw2  13031  qexpz  13050  4sqlem10  13085  ennnfonelemkh  13163  prdsbaslemss  13487  triv1nsgd  13935  qusgrp  13949  gsumsplit0  14063  bl2in  15268  xblcntrps  15278  xblcntr  15279  ssblps  15290  ssbl  15291  blssps  15292  blss  15293  xmetxp  15372  mulc1cncf  15454  cncfmptc  15461  mulcncflem  15472  ivthinclemlopn  15501  ivthinclemuopn  15503  ivthdec  15509  ivthreinc  15510  hovera  15512  hoverlt1  15514  limcimolemlt  15529  cnplimclemle  15533  cnplimclemr  15534  limccnp2lem  15541  dveflem  15591  reeff1olem  15636  reeff1oleme  15637  tangtx  15703  cosq34lt1  15715  logdivlti  15746  cxpap0  15769  rpabscxpbnd  15805  pellexlem2  15846  mersenne  15865  lgslem3  15875  gausslemma2dlem1a  15931  lgsquadlem1  15950  lgsquadlem2  15951  2lgslem1c  15963  subumgredg2en  16266  qdencn  16807  cvgcmp2nlemabs  16816  trilpolemclim  16820  trilpolemisumle  16822  trilpolemeq1  16824  apdifflemf  16830  apdifflemr  16831