Theorem eqbrtri 5112

Description: Substitution of equal classes into a binary relation. (Contributed by NM, 1-Aug-1999.)

Hypotheses

Ref	Expression
eqbrtr.1	⊢ 𝐴 = 𝐵
eqbrtr.2	⊢ 𝐵𝑅𝐶

Assertion

Ref	Expression
eqbrtri	⊢ 𝐴𝑅𝐶

Proof of Theorem eqbrtri

Step	Hyp	Ref	Expression
1		eqbrtr.2	. 2 ⊢ 𝐵𝑅𝐶
2		eqbrtr.1	. . 3 ⊢ 𝐴 = 𝐵
3	2	breq1i 5098	. 2 ⊢ (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐶)
4	1, 3	mpbir 231	1 ⊢ 𝐴𝑅𝐶

Syntax hints:   = wceq 1541   class class class wbr 5091

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-v 3438  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4284  df-if 4476  df-sn 4577  df-pr 4579  df-op 4583  df-br 5092

This theorem is referenced by:  eqbrtrri  5114  3brtr4i  5121  0sdom1dom  9130  1sdom2dom  9138  infxpenc2  9913  dju1p1e2  10065  pwsdompw  10094  r1om  10134  aleph1  10462  canthp1lem1  10543  halflt1  12338  3halfnz  12552  declei  12624  numlti  12625  sqlecan  14116  discr  14147  faclbnd3  14199  hashunlei  14332  hashge2el2dif  14387  geo2lim  15782  0.999...  15788  geoihalfsum  15789  cos2bnd  16097  sin4lt0  16104  eirrlem  16113  rpnnen2lem3  16125  rpnnen2lem9  16131  aleph1re  16154  1nprm  16590  strle2  17070  strle3  17071  1strstr  17134  2strstr  17138  rngstr  17202  srngstr  17213  lmodstr  17229  ipsstr  17240  phlstr  17250  topgrpstr  17265  otpsstr  17280  odrngstr  17307  imasvalstr  17355  chnub  18528  0frgp  19692  cnfldstr  21294  cnfldstrOLD  21309  iscmet3lem3  25218  mbfimaopnlem  25584  mbfsup  25593  mbfi1fseqlem6  25649  aalioulem3  26270  aaliou3lem3  26280  dvradcnv  26358  logi  26524  asin1  26832  log2cnv  26882  log2tlbnd  26883  mule1  27086  bposlem5  27227  bposlem8  27230  zabsle1  27235  trkgstr  28423  0pth  30103  ex-fl  30425  blocnilem  30782  norm3difi  31125  norm3adifii  31126  bcsiALT  31157  nmopsetn0  31843  nmfnsetn0  31856  nmopge0  31889  nmfnge0  31905  0bdop  31971  nmcexi  32004  opsqrlem6  32123  dp2lt10  32862  dplti  32883  dpmul4  32892  idlsrgstr  33465  locfinref  33852  dya2iocct  34291  signswch  34572  hgt750lem  34662  hgt750lem2  34663  subfaclim  35230  faclim  35788  cnndvlem1  36577  taupilem2  37362  cntotbnd  37842  60gcd7e1  42044  3lexlogpow5ineq1  42093  aks4d1p1p7  42113  acos1half  42397  diophren  42852  algstr  43212  pr2dom  43566  tr3dom  43567  binomcxplemnn0  44388  binomcxplemrat  44389  stirlinglem1  46118  dirkercncflem1  46147  fouriersw  46275  meaiunlelem  46512  ceilhalf1  47371  nfermltl2rev  47780  evengpoap3  47836  exple2lt6  48401  nnlog2ge0lt1  48604  catbas  49264  cathomfval  49265  catcofval  49266