Theorem eqbrtrd 4110

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

Syntax hints:   → wi 4   = wceq 1397   class class class wbr 4088

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-3an 1006  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-v 2804  df-un 3204  df-sn 3675  df-pr 3676  df-op 3678  df-br 4089

This theorem is referenced by:  eqbrtrrd  4112  dif1en  7067  ccfunen  7482  prarloclemcalc  7721  ltexprlemopu  7822  recexprlemloc  7850  caucvgprprlemloccalc  7903  suplocsrlem  8027  axpre-suploclemres  8120  mulle0r  9123  lbinfle  9129  divge1  9957  xltnegi  10069  xleadd1a  10107  xltadd1  10110  xlt2add  10114  xposdif  10116  xleaddadd  10121  ubmelm1fzo  10470  zsupssdc  10497  qbtwnrelemcalc  10514  qbtwnxr  10516  ceiqm1l  10572  ceilqm1lt  10573  ceilqle  10575  modqlt  10594  modqeqmodmin  10655  addmodlteq  10659  seqf1oglem1  10780  exp3vallem  10801  bernneq  10921  nn0ltexp2  10970  faclbnd2  11003  ccatsymb  11178  ccatrn  11185  resqrexlemdec  11571  resqrexlemcalc2  11575  resqrexlemglsq  11582  resqrexlemga  11583  abslt  11648  amgm2  11678  icodiamlt  11740  maxabsle  11764  maxltsup  11778  minmax  11790  min1inf  11792  min2inf  11793  bdtrilem  11799  xrmaxltsup  11818  xrmaxaddlem  11820  xrmaxadd  11821  xrminmax  11825  xrmin1inf  11827  xrmin2inf  11828  climconst  11850  serclim0  11865  mulcn2  11872  reccn2ap  11873  iserex  11899  climlec2  11901  iserge0  11903  climcau  11907  climcvg1nlem  11909  fsumabs  12025  iserabs  12035  isumlessdc  12056  divcnv  12057  expcnvre  12063  absgtap  12070  georeclim  12073  cvgratnnlembern  12083  cvgratnnlemsumlt  12088  cvgratnnlemfm  12089  cvgratnnlemrate  12090  mertenslemub  12094  mertenslemi1  12095  prodfclim1  12104  prodfap0  12105  efcvgfsum  12227  eftlub  12250  eflegeo  12261  tanval3ap  12274  tannegap  12288  ef01bndlem  12316  sin01bnd  12317  cos01bnd  12318  cos01gt0  12323  bitsfzolem  12514  bitsfzo  12515  bitsinv1lem  12521  mulgcd  12586  nnminle  12605  eucalglt  12628  lcmledvds  12641  mulgcddvds  12665  prmind2  12691  isprm5lem  12712  pw2dvdslemn  12736  pw2dvdseulemle  12738  oddpwdclemdvds  12741  sqrt2irrap  12751  divdenle  12768  nonsq  12778  pythagtriplem4  12840  pclem0  12858  pcpremul  12865  pczdvds  12886  pcprmpw2  12905  qexpz  12924  4sqlem10  12959  ennnfonelemkh  13032  prdsbaslemss  13356  triv1nsgd  13804  qusgrp  13818  bl2in  15126  xblcntrps  15136  xblcntr  15137  ssblps  15148  ssbl  15149  blssps  15150  blss  15151  xmetxp  15230  mulc1cncf  15312  cncfmptc  15319  mulcncflem  15330  ivthinclemlopn  15359  ivthinclemuopn  15361  ivthdec  15367  ivthreinc  15368  hovera  15370  hoverlt1  15372  limcimolemlt  15387  cnplimclemle  15391  cnplimclemr  15392  limccnp2lem  15399  dveflem  15449  reeff1olem  15494  reeff1oleme  15495  tangtx  15561  cosq34lt1  15573  logdivlti  15604  cxpap0  15627  rpabscxpbnd  15663  mersenne  15720  lgslem3  15730  gausslemma2dlem1a  15786  lgsquadlem1  15805  lgsquadlem2  15806  2lgslem1c  15818  subumgredg2en  16121  qdencn  16631  cvgcmp2nlemabs  16636  trilpolemclim  16640  trilpolemisumle  16642  trilpolemeq1  16644  apdifflemf  16650  apdifflemr  16651