Theorem eqbrtrd 4105

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

Syntax hints:   → wi 4   = wceq 1395   class class class wbr 4083

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-3an 1004  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-v 2801  df-un 3201  df-sn 3672  df-pr 3673  df-op 3675  df-br 4084

This theorem is referenced by:  eqbrtrrd  4107  dif1en  7049  ccfunen  7461  prarloclemcalc  7700  ltexprlemopu  7801  recexprlemloc  7829  caucvgprprlemloccalc  7882  suplocsrlem  8006  axpre-suploclemres  8099  mulle0r  9102  lbinfle  9108  divge1  9931  xltnegi  10043  xleadd1a  10081  xltadd1  10084  xlt2add  10088  xposdif  10090  xleaddadd  10095  ubmelm1fzo  10444  zsupssdc  10470  qbtwnrelemcalc  10487  qbtwnxr  10489  ceiqm1l  10545  ceilqm1lt  10546  ceilqle  10548  modqlt  10567  modqeqmodmin  10628  addmodlteq  10632  seqf1oglem1  10753  exp3vallem  10774  bernneq  10894  nn0ltexp2  10943  faclbnd2  10976  ccatsymb  11150  ccatrn  11157  resqrexlemdec  11537  resqrexlemcalc2  11541  resqrexlemglsq  11548  resqrexlemga  11549  abslt  11614  amgm2  11644  icodiamlt  11706  maxabsle  11730  maxltsup  11744  minmax  11756  min1inf  11758  min2inf  11759  bdtrilem  11765  xrmaxltsup  11784  xrmaxaddlem  11786  xrmaxadd  11787  xrminmax  11791  xrmin1inf  11793  xrmin2inf  11794  climconst  11816  serclim0  11831  mulcn2  11838  reccn2ap  11839  iserex  11865  climlec2  11867  iserge0  11869  climcau  11873  climcvg1nlem  11875  fsumabs  11991  iserabs  12001  isumlessdc  12022  divcnv  12023  expcnvre  12029  absgtap  12036  georeclim  12039  cvgratnnlembern  12049  cvgratnnlemsumlt  12054  cvgratnnlemfm  12055  cvgratnnlemrate  12056  mertenslemub  12060  mertenslemi1  12061  prodfclim1  12070  prodfap0  12071  efcvgfsum  12193  eftlub  12216  eflegeo  12227  tanval3ap  12240  tannegap  12254  ef01bndlem  12282  sin01bnd  12283  cos01bnd  12284  cos01gt0  12289  bitsfzolem  12480  bitsfzo  12481  bitsinv1lem  12487  mulgcd  12552  nnminle  12571  eucalglt  12594  lcmledvds  12607  mulgcddvds  12631  prmind2  12657  isprm5lem  12678  pw2dvdslemn  12702  pw2dvdseulemle  12704  oddpwdclemdvds  12707  sqrt2irrap  12717  divdenle  12734  nonsq  12744  pythagtriplem4  12806  pclem0  12824  pcpremul  12831  pczdvds  12852  pcprmpw2  12871  qexpz  12890  4sqlem10  12925  ennnfonelemkh  12998  prdsbaslemss  13322  triv1nsgd  13770  qusgrp  13784  bl2in  15092  xblcntrps  15102  xblcntr  15103  ssblps  15114  ssbl  15115  blssps  15116  blss  15117  xmetxp  15196  mulc1cncf  15278  cncfmptc  15285  mulcncflem  15296  ivthinclemlopn  15325  ivthinclemuopn  15327  ivthdec  15333  ivthreinc  15334  hovera  15336  hoverlt1  15338  limcimolemlt  15353  cnplimclemle  15357  cnplimclemr  15358  limccnp2lem  15365  dveflem  15415  reeff1olem  15460  reeff1oleme  15461  tangtx  15527  cosq34lt1  15539  logdivlti  15570  cxpap0  15593  rpabscxpbnd  15629  mersenne  15686  lgslem3  15696  gausslemma2dlem1a  15752  lgsquadlem1  15771  lgsquadlem2  15772  2lgslem1c  15784  qdencn  16455  cvgcmp2nlemabs  16460  trilpolemclim  16464  trilpolemisumle  16466  trilpolemeq1  16468  apdifflemf  16474  apdifflemr  16475