Theorem eqbrtri 5121

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

Syntax hints:   = wceq 1542   class class class wbr 5100

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-br 5101

This theorem is referenced by:  eqbrtrri  5123  3brtr4i  5130  0sdom1dom  9158  1sdom2dom  9166  infxpenc2  9944  dju1p1e2  10096  pwsdompw  10125  r1om  10165  aleph1  10494  canthp1lem1  10575  halflt1  12370  3halfnz  12583  declei  12655  numlti  12656  sqlecan  14144  discr  14175  faclbnd3  14227  hashunlei  14360  hashge2el2dif  14415  geo2lim  15810  0.999...  15816  geoihalfsum  15817  cos2bnd  16125  sin4lt0  16132  eirrlem  16141  rpnnen2lem3  16153  rpnnen2lem9  16159  aleph1re  16182  1nprm  16618  strle2  17098  strle3  17099  1strstr  17162  2strstr  17166  rngstr  17230  srngstr  17241  lmodstr  17257  ipsstr  17268  phlstr  17278  topgrpstr  17293  otpsstr  17308  odrngstr  17335  imasvalstr  17383  chnub  18557  0frgp  19720  cnfldstr  21323  cnfldstrOLD  21338  iscmet3lem3  25258  mbfimaopnlem  25624  mbfsup  25633  mbfi1fseqlem6  25689  aalioulem3  26310  aaliou3lem3  26320  dvradcnv  26398  logi  26564  asin1  26872  log2cnv  26922  log2tlbnd  26923  mule1  27126  bposlem5  27267  bposlem8  27270  zabsle1  27275  trkgstr  28528  0pth  30212  ex-fl  30534  blocnilem  30891  norm3difi  31234  norm3adifii  31235  bcsiALT  31266  nmopsetn0  31952  nmfnsetn0  31965  nmopge0  31998  nmfnge0  32014  0bdop  32080  nmcexi  32113  opsqrlem6  32232  dp2lt10  32975  dplti  32996  dpmul4  33005  idlsrgstr  33594  locfinref  34018  dya2iocct  34457  signswch  34738  hgt750lem  34828  hgt750lem2  34829  subfaclim  35401  faclim  35959  cnndvlem1  36756  taupilem2  37574  cntotbnd  38044  60gcd7e1  42372  3lexlogpow5ineq1  42421  aks4d1p1p7  42441  acos1half  42725  diophren  43167  algstr  43527  pr2dom  43880  tr3dom  43881  binomcxplemnn0  44702  binomcxplemrat  44703  stirlinglem1  46429  dirkercncflem1  46458  fouriersw  46586  meaiunlelem  46823  nthrucw  47241  ceilhalf1  47691  nfermltl2rev  48100  evengpoap3  48156  exple2lt6  48721  nnlog2ge0lt1  48923  catbas  49582  cathomfval  49583  catcofval  49584