Theorem eqbrtrd 3998

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

Syntax hints:   → wi 4   = wceq 1342   class class class wbr 3976

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1434  ax-7 1435  ax-gen 1436  ax-ie1 1480  ax-ie2 1481  ax-8 1491  ax-10 1492  ax-11 1493  ax-i12 1494  ax-bndl 1496  ax-4 1497  ax-17 1513  ax-i9 1517  ax-ial 1521  ax-i5r 1522  ax-ext 2146

This theorem depends on definitions:  df-bi 116  df-3an 969  df-tru 1345  df-nf 1448  df-sb 1750  df-clab 2151  df-cleq 2157  df-clel 2160  df-nfc 2295  df-v 2723  df-un 3115  df-sn 3576  df-pr 3577  df-op 3579  df-br 3977

This theorem is referenced by:  eqbrtrrd  4000  dif1en  6836  ccfunen  7196  prarloclemcalc  7434  ltexprlemopu  7535  recexprlemloc  7563  caucvgprprlemloccalc  7616  suplocsrlem  7740  axpre-suploclemres  7833  mulle0r  8830  lbinfle  8836  divge1  9650  xltnegi  9762  xleadd1a  9800  xltadd1  9803  xlt2add  9807  xposdif  9809  xleaddadd  9814  ubmelm1fzo  10151  qbtwnrelemcalc  10181  qbtwnxr  10183  ceiqm1l  10236  ceilqm1lt  10237  ceilqle  10239  modqlt  10258  modqeqmodmin  10319  addmodlteq  10323  exp3vallem  10446  bernneq  10564  nn0ltexp2  10612  faclbnd2  10644  resqrexlemdec  10939  resqrexlemcalc2  10943  resqrexlemglsq  10950  resqrexlemga  10951  abslt  11016  amgm2  11046  icodiamlt  11108  maxabsle  11132  maxltsup  11146  minmax  11157  min1inf  11159  min2inf  11160  bdtrilem  11166  xrmaxltsup  11185  xrmaxaddlem  11187  xrmaxadd  11188  xrminmax  11192  xrmin1inf  11194  xrmin2inf  11195  climconst  11217  serclim0  11232  mulcn2  11239  reccn2ap  11240  iserex  11266  climlec2  11268  iserge0  11270  climcau  11274  climcvg1nlem  11276  fsumabs  11392  iserabs  11402  isumlessdc  11423  divcnv  11424  expcnvre  11430  absgtap  11437  georeclim  11440  cvgratnnlembern  11450  cvgratnnlemsumlt  11455  cvgratnnlemfm  11456  cvgratnnlemrate  11457  mertenslemub  11461  mertenslemi1  11462  prodfclim1  11471  prodfap0  11472  efcvgfsum  11594  eftlub  11617  eflegeo  11628  tanval3ap  11641  tannegap  11655  ef01bndlem  11683  sin01bnd  11684  cos01bnd  11685  cos01gt0  11689  zsupssdc  11872  mulgcd  11934  eucalglt  11968  lcmledvds  11981  mulgcddvds  12005  prmind2  12031  pw2dvdslemn  12074  pw2dvdseulemle  12076  oddpwdclemdvds  12079  sqrt2irrap  12089  divdenle  12106  nonsq  12116  pythagtriplem4  12177  pclem0  12195  pcpremul  12202  pczdvds  12222  pcprmpw2  12241  qexpz  12259  ennnfonelemkh  12282  nnminle  12319  bl2in  12944  xblcntrps  12954  xblcntr  12955  ssblps  12966  ssbl  12967  blssps  12968  blss  12969  xmetxp  13048  mulc1cncf  13117  cncfmptc  13123  mulcncflem  13131  ivthinclemlopn  13155  ivthinclemuopn  13157  ivthdec  13163  limcimolemlt  13174  cnplimclemle  13178  cnplimclemr  13179  limccnp2lem  13186  dveflem  13228  reeff1olem  13233  reeff1oleme  13234  tangtx  13300  cosq34lt1  13312  logdivlti  13343  cxpap0  13366  rpabscxpbnd  13400  qdencn  13740  cvgcmp2nlemabs  13745  trilpolemclim  13749  trilpolemisumle  13751  trilpolemeq1  13753  apdifflemf  13759  apdifflemr  13760