Theorem eqbrtrd 3950

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

Syntax hints:   → wi 4   = wceq 1331   class class class wbr 3929

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 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121

This theorem depends on definitions:  df-bi 116  df-3an 964  df-tru 1334  df-nf 1437  df-sb 1736  df-clab 2126  df-cleq 2132  df-clel 2135  df-nfc 2270  df-v 2688  df-un 3075  df-sn 3533  df-pr 3534  df-op 3536  df-br 3930

This theorem is referenced by:  eqbrtrrd  3952  dif1en  6773  ccfunen  7079  prarloclemcalc  7310  ltexprlemopu  7411  recexprlemloc  7439  caucvgprprlemloccalc  7492  suplocsrlem  7616  axpre-suploclemres  7709  mulle0r  8702  lbinfle  8708  divge1  9510  xltnegi  9618  xleadd1a  9656  xltadd1  9659  xlt2add  9663  xposdif  9665  xleaddadd  9670  ubmelm1fzo  10003  qbtwnrelemcalc  10033  qbtwnxr  10035  ceiqm1l  10084  ceilqm1lt  10085  ceilqle  10087  modqlt  10106  modqeqmodmin  10167  addmodlteq  10171  exp3vallem  10294  bernneq  10412  faclbnd2  10488  resqrexlemdec  10783  resqrexlemcalc2  10787  resqrexlemglsq  10794  resqrexlemga  10795  abslt  10860  amgm2  10890  icodiamlt  10952  maxabsle  10976  maxltsup  10990  minmax  11001  min1inf  11003  min2inf  11004  bdtrilem  11010  xrmaxltsup  11027  xrmaxaddlem  11029  xrmaxadd  11030  xrminmax  11034  xrmin1inf  11036  xrmin2inf  11037  climconst  11059  serclim0  11074  mulcn2  11081  reccn2ap  11082  iserex  11108  climlec2  11110  iserge0  11112  climcau  11116  climcvg1nlem  11118  fsumabs  11234  iserabs  11244  isumlessdc  11265  divcnv  11266  expcnvre  11272  absgtap  11279  georeclim  11282  cvgratnnlembern  11292  cvgratnnlemsumlt  11297  cvgratnnlemfm  11298  cvgratnnlemrate  11299  mertenslemub  11303  mertenslemi1  11304  prodfclim1  11313  prodfap0  11314  efcvgfsum  11373  eftlub  11396  eflegeo  11408  tanval3ap  11421  tannegap  11435  ef01bndlem  11463  sin01bnd  11464  cos01bnd  11465  cos01gt0  11469  mulgcd  11704  eucalglt  11738  lcmledvds  11751  mulgcddvds  11775  prmind2  11801  pw2dvdslemn  11843  pw2dvdseulemle  11845  oddpwdclemdvds  11848  sqrt2irrap  11858  divdenle  11875  nonsq  11885  ennnfonelemkh  11925  bl2in  12572  xblcntrps  12582  xblcntr  12583  ssblps  12594  ssbl  12595  blssps  12596  blss  12597  xmetxp  12676  mulc1cncf  12745  cncfmptc  12751  mulcncflem  12759  ivthinclemlopn  12783  ivthinclemuopn  12785  ivthdec  12791  limcimolemlt  12802  cnplimclemle  12806  cnplimclemr  12807  limccnp2lem  12814  dveflem  12855  tangtx  12919  cosq34lt1  12931  qdencn  13222  cvgcmp2nlemabs  13227  trilpolemclim  13229  trilpolemisumle  13231  trilpolemeq1  13233