Theorem eqbrtrd 4115

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

Syntax hints:   → wi 4   = wceq 1398   class class class wbr 4093

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2364  df-v 2805  df-un 3205  df-sn 3679  df-pr 3680  df-op 3682  df-br 4094

This theorem is referenced by:  eqbrtrrd  4117  dif1en  7111  ccfunen  7526  prarloclemcalc  7765  ltexprlemopu  7866  recexprlemloc  7894  caucvgprprlemloccalc  7947  suplocsrlem  8071  axpre-suploclemres  8164  mulle0r  9166  lbinfle  9172  divge1  10002  xltnegi  10114  xleadd1a  10152  xltadd1  10155  xlt2add  10159  xposdif  10161  xleaddadd  10166  lincmble  10283  ubmelm1fzo  10517  zsupssdc  10544  qbtwnrelemcalc  10561  qbtwnxr  10563  ceiqm1l  10619  ceilqm1lt  10620  ceilqle  10622  modqlt  10641  modqeqmodmin  10702  addmodlteq  10706  seqf1oglem1  10827  exp3vallem  10848  bernneq  10968  nn0ltexp2  11017  faclbnd2  11050  ccatsymb  11228  ccatrn  11235  resqrexlemdec  11634  resqrexlemcalc2  11638  resqrexlemglsq  11645  resqrexlemga  11646  abslt  11711  amgm2  11741  icodiamlt  11803  maxabsle  11827  maxltsup  11841  minmax  11853  min1inf  11855  min2inf  11856  bdtrilem  11862  xrmaxltsup  11881  xrmaxaddlem  11883  xrmaxadd  11884  xrminmax  11888  xrmin1inf  11890  xrmin2inf  11891  climconst  11913  serclim0  11928  mulcn2  11935  reccn2ap  11936  iserex  11962  climlec2  11964  iserge0  11966  climcau  11970  climcvg1nlem  11972  fsumabs  12089  iserabs  12099  isumlessdc  12120  divcnv  12121  expcnvre  12127  absgtap  12134  georeclim  12137  cvgratnnlembern  12147  cvgratnnlemsumlt  12152  cvgratnnlemfm  12153  cvgratnnlemrate  12154  mertenslemub  12158  mertenslemi1  12159  prodfclim1  12168  prodfap0  12169  efcvgfsum  12291  eftlub  12314  eflegeo  12325  tanval3ap  12338  tannegap  12352  ef01bndlem  12380  sin01bnd  12381  cos01bnd  12382  cos01gt0  12387  bitsfzolem  12578  bitsfzo  12579  bitsinv1lem  12585  mulgcd  12650  nnminle  12669  eucalglt  12692  lcmledvds  12705  mulgcddvds  12729  prmind2  12755  isprm5lem  12776  pw2dvdslemn  12800  pw2dvdseulemle  12802  oddpwdclemdvds  12805  sqrt2irrap  12815  divdenle  12832  nonsq  12842  pythagtriplem4  12904  pclem0  12922  pcpremul  12929  pczdvds  12950  pcprmpw2  12969  qexpz  12988  4sqlem10  13023  ennnfonelemkh  13096  prdsbaslemss  13420  triv1nsgd  13868  qusgrp  13882  gsumsplit0  13996  bl2in  15197  xblcntrps  15207  xblcntr  15208  ssblps  15219  ssbl  15220  blssps  15221  blss  15222  xmetxp  15301  mulc1cncf  15383  cncfmptc  15390  mulcncflem  15401  ivthinclemlopn  15430  ivthinclemuopn  15432  ivthdec  15438  ivthreinc  15439  hovera  15441  hoverlt1  15443  limcimolemlt  15458  cnplimclemle  15462  cnplimclemr  15463  limccnp2lem  15470  dveflem  15520  reeff1olem  15565  reeff1oleme  15566  tangtx  15632  cosq34lt1  15644  logdivlti  15675  cxpap0  15698  rpabscxpbnd  15734  pellexlem2  15775  mersenne  15794  lgslem3  15804  gausslemma2dlem1a  15860  lgsquadlem1  15879  lgsquadlem2  15880  2lgslem1c  15892  subumgredg2en  16195  qdencn  16738  cvgcmp2nlemabs  16747  trilpolemclim  16751  trilpolemisumle  16753  trilpolemeq1  16755  apdifflemf  16761  apdifflemr  16762