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  11264  resqrexlemcalc2  11268  resqrexlemglsq  11275  resqrexlemga  11276  abslt  11341  amgm2  11371  icodiamlt  11433  maxabsle  11457  maxltsup  11471  minmax  11483  min1inf  11485  min2inf  11486  bdtrilem  11492  xrmaxltsup  11511  xrmaxaddlem  11513  xrmaxadd  11514  xrminmax  11518  xrmin1inf  11520  xrmin2inf  11521  climconst  11543  serclim0  11558  mulcn2  11565  reccn2ap  11566  iserex  11592  climlec2  11594  iserge0  11596  climcau  11600  climcvg1nlem  11602  fsumabs  11718  iserabs  11728  isumlessdc  11749  divcnv  11750  expcnvre  11756  absgtap  11763  georeclim  11766  cvgratnnlembern  11776  cvgratnnlemsumlt  11781  cvgratnnlemfm  11782  cvgratnnlemrate  11783  mertenslemub  11787  mertenslemi1  11788  prodfclim1  11797  prodfap0  11798  efcvgfsum  11920  eftlub  11943  eflegeo  11954  tanval3ap  11967  tannegap  11981  ef01bndlem  12009  sin01bnd  12010  cos01bnd  12011  cos01gt0  12016  bitsfzolem  12207  bitsfzo  12208  bitsinv1lem  12214  mulgcd  12279  nnminle  12298  eucalglt  12321  lcmledvds  12334  mulgcddvds  12358  prmind2  12384  isprm5lem  12405  pw2dvdslemn  12429  pw2dvdseulemle  12431  oddpwdclemdvds  12434  sqrt2irrap  12444  divdenle  12461  nonsq  12471  pythagtriplem4  12533  pclem0  12551  pcpremul  12558  pczdvds  12579  pcprmpw2  12598  qexpz  12617  4sqlem10  12652  ennnfonelemkh  12725  prdsbaslemss  13048  triv1nsgd  13496  qusgrp  13510  bl2in  14817  xblcntrps  14827  xblcntr  14828  ssblps  14839  ssbl  14840  blssps  14841  blss  14842  xmetxp  14921  mulc1cncf  15003  cncfmptc  15010  mulcncflem  15021  ivthinclemlopn  15050  ivthinclemuopn  15052  ivthdec  15058  ivthreinc  15059  hovera  15061  hoverlt1  15063  limcimolemlt  15078  cnplimclemle  15082  cnplimclemr  15083  limccnp2lem  15090  dveflem  15140  reeff1olem  15185  reeff1oleme  15186  tangtx  15252  cosq34lt1  15264  logdivlti  15295  cxpap0  15318  rpabscxpbnd  15354  mersenne  15411  lgslem3  15421  gausslemma2dlem1a  15477  lgsquadlem1  15496  lgsquadlem2  15497  2lgslem1c  15509  qdencn  15899  cvgcmp2nlemabs  15904  trilpolemclim  15908  trilpolemisumle  15910  trilpolemeq1  15912  apdifflemf  15918  apdifflemr  15919