Theorem eqbrtrd 4020

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

Syntax hints:   → wi 4   = wceq 1353   class class class wbr 3998

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 709  ax-5 1445  ax-7 1446  ax-gen 1447  ax-ie1 1491  ax-ie2 1492  ax-8 1502  ax-10 1503  ax-11 1504  ax-i12 1505  ax-bndl 1507  ax-4 1508  ax-17 1524  ax-i9 1528  ax-ial 1532  ax-i5r 1533  ax-ext 2157

This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1459  df-sb 1761  df-clab 2162  df-cleq 2168  df-clel 2171  df-nfc 2306  df-v 2737  df-un 3131  df-sn 3595  df-pr 3596  df-op 3598  df-br 3999

This theorem is referenced by:  eqbrtrrd  4022  dif1en  6869  ccfunen  7238  prarloclemcalc  7476  ltexprlemopu  7577  recexprlemloc  7605  caucvgprprlemloccalc  7658  suplocsrlem  7782  axpre-suploclemres  7875  mulle0r  8874  lbinfle  8880  divge1  9694  xltnegi  9806  xleadd1a  9844  xltadd1  9847  xlt2add  9851  xposdif  9853  xleaddadd  9858  ubmelm1fzo  10196  qbtwnrelemcalc  10226  qbtwnxr  10228  ceiqm1l  10281  ceilqm1lt  10282  ceilqle  10284  modqlt  10303  modqeqmodmin  10364  addmodlteq  10368  exp3vallem  10491  bernneq  10610  nn0ltexp2  10658  faclbnd2  10690  resqrexlemdec  10988  resqrexlemcalc2  10992  resqrexlemglsq  10999  resqrexlemga  11000  abslt  11065  amgm2  11095  icodiamlt  11157  maxabsle  11181  maxltsup  11195  minmax  11206  min1inf  11208  min2inf  11209  bdtrilem  11215  xrmaxltsup  11234  xrmaxaddlem  11236  xrmaxadd  11237  xrminmax  11241  xrmin1inf  11243  xrmin2inf  11244  climconst  11266  serclim0  11281  mulcn2  11288  reccn2ap  11289  iserex  11315  climlec2  11317  iserge0  11319  climcau  11323  climcvg1nlem  11325  fsumabs  11441  iserabs  11451  isumlessdc  11472  divcnv  11473  expcnvre  11479  absgtap  11486  georeclim  11489  cvgratnnlembern  11499  cvgratnnlemsumlt  11504  cvgratnnlemfm  11505  cvgratnnlemrate  11506  mertenslemub  11510  mertenslemi1  11511  prodfclim1  11520  prodfap0  11521  efcvgfsum  11643  eftlub  11666  eflegeo  11677  tanval3ap  11690  tannegap  11704  ef01bndlem  11732  sin01bnd  11733  cos01bnd  11734  cos01gt0  11738  zsupssdc  11922  mulgcd  11984  nnminle  12003  eucalglt  12024  lcmledvds  12037  mulgcddvds  12061  prmind2  12087  isprm5lem  12108  pw2dvdslemn  12132  pw2dvdseulemle  12134  oddpwdclemdvds  12137  sqrt2irrap  12147  divdenle  12164  nonsq  12174  pythagtriplem4  12235  pclem0  12253  pcpremul  12260  pczdvds  12280  pcprmpw2  12299  qexpz  12317  4sqlem10  12352  ennnfonelemkh  12380  bl2in  13474  xblcntrps  13484  xblcntr  13485  ssblps  13496  ssbl  13497  blssps  13498  blss  13499  xmetxp  13578  mulc1cncf  13647  cncfmptc  13653  mulcncflem  13661  ivthinclemlopn  13685  ivthinclemuopn  13687  ivthdec  13693  limcimolemlt  13704  cnplimclemle  13708  cnplimclemr  13709  limccnp2lem  13716  dveflem  13758  reeff1olem  13763  reeff1oleme  13764  tangtx  13830  cosq34lt1  13842  logdivlti  13873  cxpap0  13896  rpabscxpbnd  13930  lgslem3  13974  qdencn  14336  cvgcmp2nlemabs  14341  trilpolemclim  14345  trilpolemisumle  14347  trilpolemeq1  14349  apdifflemf  14355  apdifflemr  14356