Theorem eqbrtri 5118

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

Syntax hints:   = wceq 1559   class class class wbr 5097

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3455  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4284  df-if 4478  df-sn 4580  df-pr 4582  df-op 4586  df-br 5098

This theorem is referenced by:  eqbrtrri  5120  3brtr4i  5127  0sdom1dom  9183  1sdom2dom  9191  infxpenc2  9971  dju1p1e2  10123  pwsdompw  10152  r1om  10192  aleph1  10522  canthp1lem1  10603  halflt1  12431  3halfnz  12645  declei  12722  numlti  12723  sqlecan  14215  discr  14246  faclbnd3  14298  hashunlei  14431  hashge2el2dif  14486  geo2lim  15895  0.999...  15901  geoihalfsum  15902  cos2bnd  16210  sin4lt0  16217  eirrlem  16226  rpnnen2lem3  16238  rpnnen2lem9  16244  aleph1re  16267  1nprm  16703  strle2  17185  strle3  17186  1strstr  17249  2strstr  17253  rngstr  17317  srngstr  17328  lmodstr  17344  ipsstr  17355  phlstr  17365  topgrpstr  17380  otpsstr  17395  odrngstr  17422  imasvalstr  17470  chnub  18644  0frgp  19809  cnfldstr  21413  iscmet3lem3  25339  mbfimaopnlem  25704  mbfsup  25713  mbfi1fseqlem6  25769  aalioulem3  26385  aaliou3lem3  26395  dvradcnv  26471  logi  26639  asin1  26946  log2cnv  26996  log2tlbnd  26997  mule1  27199  bposlem5  27339  bposlem8  27342  zabsle1  27347  trkgstr  28600  0pth  30283  ex-fl  30605  blocnilem  30963  norm3difi  31306  norm3adifii  31307  bcsiALT  31338  nmopsetn0  32024  nmfnsetn0  32037  nmopge0  32070  nmfnge0  32086  0bdop  32152  nmcexi  32185  opsqrlem6  32304  dp2lt10  33021  dplti  33042  dpmul4  33051  idlsrgstr  33658  locfinref  34098  dya2iocct  34537  signswch  34815  hgt750lem  34905  hgt750lem2  34906  subfaclim  35498  faclim  36056  cnndvlem1  36935  taupilem2  37774  cntotbnd  38255  60gcd7e1  42582  3lexlogpow5ineq1  42631  aks4d1p1p7  42651  acos1half  42927  diophren  43350  algstr  43710  pr2dom  44063  tr3dom  44064  binomcxplemnn0  44885  binomcxplemrat  44886  stirlinglem1  46608  dirkercncflem1  46637  fouriersw  46765  meaiunlelem  47002  nthrucw  47422  ceilhalf1  47892  nfermltl2rev  48325  evengpoap3  48381  exple2lt6  48946  nnlog2ge0lt1  49148  catbas  49807  cathomfval  49808  catcofval  49809