Theorem eqbrtri 5128

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 5114	. 2 ⊢ (𝐴𝑅𝐶 ↔ 𝐵𝑅𝐶)
4	1, 3	mpbir 231	1 ⊢ 𝐴𝑅𝐶

Syntax hints:   = wceq 1540   class class class wbr 5107

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-br 5108

This theorem is referenced by:  eqbrtrri  5130  3brtr4i  5137  0sdom1dom  9185  1sdom2dom  9194  infxpenc2  9975  dju1p1e2  10127  pwsdompw  10156  r1om  10196  aleph1  10524  canthp1lem1  10605  halflt1  12399  3halfnz  12613  declei  12685  numlti  12686  sqlecan  14174  discr  14205  faclbnd3  14257  hashunlei  14390  hashge2el2dif  14445  geo2lim  15841  0.999...  15847  geoihalfsum  15848  cos2bnd  16156  sin4lt0  16163  eirrlem  16172  rpnnen2lem3  16184  rpnnen2lem9  16190  aleph1re  16213  1nprm  16649  strle2  17129  strle3  17130  1strstr  17193  2strstr  17197  rngstr  17261  srngstr  17272  lmodstr  17288  ipsstr  17299  phlstr  17309  topgrpstr  17324  otpsstr  17339  odrngstr  17366  imasvalstr  17414  0frgp  19709  cnfldstr  21266  cnfldstrOLD  21281  iscmet3lem3  25190  mbfimaopnlem  25556  mbfsup  25565  mbfi1fseqlem6  25621  aalioulem3  26242  aaliou3lem3  26252  dvradcnv  26330  logi  26496  asin1  26804  log2cnv  26854  log2tlbnd  26855  mule1  27058  bposlem5  27199  bposlem8  27202  zabsle1  27207  trkgstr  28371  0pth  30054  ex-fl  30376  blocnilem  30733  norm3difi  31076  norm3adifii  31077  bcsiALT  31108  nmopsetn0  31794  nmfnsetn0  31807  nmopge0  31840  nmfnge0  31856  0bdop  31922  nmcexi  31955  opsqrlem6  32074  dp2lt10  32804  dplti  32825  dpmul4  32834  chnub  32938  idlsrgstr  33473  locfinref  33831  dya2iocct  34271  signswch  34552  hgt750lem  34642  hgt750lem2  34643  subfaclim  35175  faclim  35733  cnndvlem1  36525  taupilem2  37310  cntotbnd  37790  60gcd7e1  41993  3lexlogpow5ineq1  42042  aks4d1p1p7  42062  acos1half  42346  diophren  42801  algstr  43162  pr2dom  43516  tr3dom  43517  binomcxplemnn0  44338  binomcxplemrat  44339  stirlinglem1  46072  dirkercncflem1  46101  fouriersw  46229  meaiunlelem  46466  ceilhalf1  47335  nfermltl2rev  47744  evengpoap3  47800  exple2lt6  48352  nnlog2ge0lt1  48555  catbas  49215  cathomfval  49216  catcofval  49217