Theorem eqbrtri 5125

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

Syntax hints:   = wceq 1563   class class class wbr 5104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-rab 3418  df-v 3459  df-dif 3910  df-un 3912  df-ss 3924  df-nul 4289  df-if 4484  df-sn 4586  df-pr 4588  df-op 4592  df-br 5105

This theorem is referenced by:  eqbrtrri  5127  3brtr4i  5134  0sdom1dom  9194  1sdom2dom  9202  infxpenc2  9994  dju1p1e2  10145  pwsdompw  10174  r1om  10214  aleph1  10544  canthp1lem1  10625  halflt1  12449  3halfnz  12663  declei  12740  numlti  12741  sqlecan  14233  discr  14264  faclbnd3  14316  hashunlei  14450  hashge2el2dif  14505  geo2lim  15917  0.999...  15923  geoihalfsum  15924  cos2bnd  16232  sin4lt0  16239  eirrlem  16248  rpnnen2lem3  16260  rpnnen2lem9  16266  aleph1re  16289  1nprm  16725  strle2  17207  strle3  17208  1strstr  17271  2strstr  17275  rngstr  17339  srngstr  17350  lmodstr  17366  ipsstr  17377  phlstr  17387  topgrpstr  17402  otpsstr  17417  odrngstr  17444  imasvalstr  17492  chnub  18666  0frgp  19837  cnfldstr  21481  iscmet3lem3  25406  mbfimaopnlem  25771  mbfsup  25780  mbfi1fseqlem6  25836  aalioulem3  26452  aaliou3lem3  26462  dvradcnv  26538  logi  26706  asin1  27013  log2cnv  27063  log2tlbnd  27064  mule1  27266  bposlem5  27406  bposlem8  27409  zabsle1  27414  trkgstr  28667  0pth  30381  ex-fl  30703  blocnilem  31061  norm3difi  31404  norm3adifii  31405  bcsiALT  31436  nmopsetn0  32122  nmfnsetn0  32135  nmopge0  32168  nmfnge0  32184  0bdop  32250  nmcexi  32283  opsqrlem6  32402  dp2lt10  33111  dplti  33132  dpmul4  33141  idlsrgstr  33704  locfinref  34143  dya2iocct  34582  signswch  34860  hgt750lem  34950  hgt750lem2  34951  subfaclim  35546  faclim  36104  cnndvlem1  36983  taupilem2  37821  cntotbnd  38302  60gcd7e1  42629  3lexlogpow5ineq1  42678  aks4d1p1p7  42698  acos1half  42974  diophren  43397  algstr  43757  pr2dom  44110  tr3dom  44111  binomcxplemnn0  44918  binomcxplemrat  44919  stirlinglem1  46647  dirkercncflem1  46676  fouriersw  46804  meaiunlelem  47041  nthrucw  47461  ceilhalf1  47931  nfermltl2rev  48364  evengpoap3  48420  exple2lt6  48996  nnlog2ge0lt1  49198  catbas  49856  cathomfval  49857  catcofval  49858