Theorem eqbrtrd 4066

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

Syntax hints:   → wi 4   = wceq 1373   class class class wbr 4044

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 711  ax-5 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-10 1528  ax-11 1529  ax-i12 1530  ax-bndl 1532  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-3an 983  df-tru 1376  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-nfc 2337  df-v 2774  df-un 3170  df-sn 3639  df-pr 3640  df-op 3642  df-br 4045

This theorem is referenced by:  eqbrtrrd  4068  dif1en  6976  ccfunen  7376  prarloclemcalc  7615  ltexprlemopu  7716  recexprlemloc  7744  caucvgprprlemloccalc  7797  suplocsrlem  7921  axpre-suploclemres  8014  mulle0r  9017  lbinfle  9023  divge1  9845  xltnegi  9957  xleadd1a  9995  xltadd1  9998  xlt2add  10002  xposdif  10004  xleaddadd  10009  ubmelm1fzo  10355  zsupssdc  10381  qbtwnrelemcalc  10398  qbtwnxr  10400  ceiqm1l  10456  ceilqm1lt  10457  ceilqle  10459  modqlt  10478  modqeqmodmin  10539  addmodlteq  10543  seqf1oglem1  10664  exp3vallem  10685  bernneq  10805  nn0ltexp2  10854  faclbnd2  10887  ccatsymb  11058  ccatrn  11065  resqrexlemdec  11322  resqrexlemcalc2  11326  resqrexlemglsq  11333  resqrexlemga  11334  abslt  11399  amgm2  11429  icodiamlt  11491  maxabsle  11515  maxltsup  11529  minmax  11541  min1inf  11543  min2inf  11544  bdtrilem  11550  xrmaxltsup  11569  xrmaxaddlem  11571  xrmaxadd  11572  xrminmax  11576  xrmin1inf  11578  xrmin2inf  11579  climconst  11601  serclim0  11616  mulcn2  11623  reccn2ap  11624  iserex  11650  climlec2  11652  iserge0  11654  climcau  11658  climcvg1nlem  11660  fsumabs  11776  iserabs  11786  isumlessdc  11807  divcnv  11808  expcnvre  11814  absgtap  11821  georeclim  11824  cvgratnnlembern  11834  cvgratnnlemsumlt  11839  cvgratnnlemfm  11840  cvgratnnlemrate  11841  mertenslemub  11845  mertenslemi1  11846  prodfclim1  11855  prodfap0  11856  efcvgfsum  11978  eftlub  12001  eflegeo  12012  tanval3ap  12025  tannegap  12039  ef01bndlem  12067  sin01bnd  12068  cos01bnd  12069  cos01gt0  12074  bitsfzolem  12265  bitsfzo  12266  bitsinv1lem  12272  mulgcd  12337  nnminle  12356  eucalglt  12379  lcmledvds  12392  mulgcddvds  12416  prmind2  12442  isprm5lem  12463  pw2dvdslemn  12487  pw2dvdseulemle  12489  oddpwdclemdvds  12492  sqrt2irrap  12502  divdenle  12519  nonsq  12529  pythagtriplem4  12591  pclem0  12609  pcpremul  12616  pczdvds  12637  pcprmpw2  12656  qexpz  12675  4sqlem10  12710  ennnfonelemkh  12783  prdsbaslemss  13106  triv1nsgd  13554  qusgrp  13568  bl2in  14875  xblcntrps  14885  xblcntr  14886  ssblps  14897  ssbl  14898  blssps  14899  blss  14900  xmetxp  14979  mulc1cncf  15061  cncfmptc  15068  mulcncflem  15079  ivthinclemlopn  15108  ivthinclemuopn  15110  ivthdec  15116  ivthreinc  15117  hovera  15119  hoverlt1  15121  limcimolemlt  15136  cnplimclemle  15140  cnplimclemr  15141  limccnp2lem  15148  dveflem  15198  reeff1olem  15243  reeff1oleme  15244  tangtx  15310  cosq34lt1  15322  logdivlti  15353  cxpap0  15376  rpabscxpbnd  15412  mersenne  15469  lgslem3  15479  gausslemma2dlem1a  15535  lgsquadlem1  15554  lgsquadlem2  15555  2lgslem1c  15567  qdencn  15966  cvgcmp2nlemabs  15971  trilpolemclim  15975  trilpolemisumle  15977  trilpolemeq1  15979  apdifflemf  15985  apdifflemr  15986