Theorem eqbrtrd 4065

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

Syntax hints:   → wi 4   = wceq 1372   class class class wbr 4043

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 710  ax-5 1469  ax-7 1470  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-8 1526  ax-10 1527  ax-11 1528  ax-i12 1529  ax-bndl 1531  ax-4 1532  ax-17 1548  ax-i9 1552  ax-ial 1556  ax-i5r 1557  ax-ext 2186

This theorem depends on definitions:  df-bi 117  df-3an 982  df-tru 1375  df-nf 1483  df-sb 1785  df-clab 2191  df-cleq 2197  df-clel 2200  df-nfc 2336  df-v 2773  df-un 3169  df-sn 3638  df-pr 3639  df-op 3641  df-br 4044

This theorem is referenced by:  eqbrtrrd  4067  dif1en  6975  ccfunen  7375  prarloclemcalc  7614  ltexprlemopu  7715  recexprlemloc  7743  caucvgprprlemloccalc  7796  suplocsrlem  7920  axpre-suploclemres  8013  mulle0r  9016  lbinfle  9022  divge1  9844  xltnegi  9956  xleadd1a  9994  xltadd1  9997  xlt2add  10001  xposdif  10003  xleaddadd  10008  ubmelm1fzo  10353  zsupssdc  10379  qbtwnrelemcalc  10396  qbtwnxr  10398  ceiqm1l  10454  ceilqm1lt  10455  ceilqle  10457  modqlt  10476  modqeqmodmin  10537  addmodlteq  10541  seqf1oglem1  10662  exp3vallem  10683  bernneq  10803  nn0ltexp2  10852  faclbnd2  10885  ccatsymb  11056  ccatrn  11063  resqrexlemdec  11293  resqrexlemcalc2  11297  resqrexlemglsq  11304  resqrexlemga  11305  abslt  11370  amgm2  11400  icodiamlt  11462  maxabsle  11486  maxltsup  11500  minmax  11512  min1inf  11514  min2inf  11515  bdtrilem  11521  xrmaxltsup  11540  xrmaxaddlem  11542  xrmaxadd  11543  xrminmax  11547  xrmin1inf  11549  xrmin2inf  11550  climconst  11572  serclim0  11587  mulcn2  11594  reccn2ap  11595  iserex  11621  climlec2  11623  iserge0  11625  climcau  11629  climcvg1nlem  11631  fsumabs  11747  iserabs  11757  isumlessdc  11778  divcnv  11779  expcnvre  11785  absgtap  11792  georeclim  11795  cvgratnnlembern  11805  cvgratnnlemsumlt  11810  cvgratnnlemfm  11811  cvgratnnlemrate  11812  mertenslemub  11816  mertenslemi1  11817  prodfclim1  11826  prodfap0  11827  efcvgfsum  11949  eftlub  11972  eflegeo  11983  tanval3ap  11996  tannegap  12010  ef01bndlem  12038  sin01bnd  12039  cos01bnd  12040  cos01gt0  12045  bitsfzolem  12236  bitsfzo  12237  bitsinv1lem  12243  mulgcd  12308  nnminle  12327  eucalglt  12350  lcmledvds  12363  mulgcddvds  12387  prmind2  12413  isprm5lem  12434  pw2dvdslemn  12458  pw2dvdseulemle  12460  oddpwdclemdvds  12463  sqrt2irrap  12473  divdenle  12490  nonsq  12500  pythagtriplem4  12562  pclem0  12580  pcpremul  12587  pczdvds  12608  pcprmpw2  12627  qexpz  12646  4sqlem10  12681  ennnfonelemkh  12754  prdsbaslemss  13077  triv1nsgd  13525  qusgrp  13539  bl2in  14846  xblcntrps  14856  xblcntr  14857  ssblps  14868  ssbl  14869  blssps  14870  blss  14871  xmetxp  14950  mulc1cncf  15032  cncfmptc  15039  mulcncflem  15050  ivthinclemlopn  15079  ivthinclemuopn  15081  ivthdec  15087  ivthreinc  15088  hovera  15090  hoverlt1  15092  limcimolemlt  15107  cnplimclemle  15111  cnplimclemr  15112  limccnp2lem  15119  dveflem  15169  reeff1olem  15214  reeff1oleme  15215  tangtx  15281  cosq34lt1  15293  logdivlti  15324  cxpap0  15347  rpabscxpbnd  15383  mersenne  15440  lgslem3  15450  gausslemma2dlem1a  15506  lgsquadlem1  15525  lgsquadlem2  15526  2lgslem1c  15538  qdencn  15928  cvgcmp2nlemabs  15933  trilpolemclim  15937  trilpolemisumle  15939  trilpolemeq1  15941  apdifflemf  15947  apdifflemr  15948