Theorem eqbrtri 5107

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

Syntax hints:   = wceq 1542   class class class wbr 5086

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 3391  df-v 3432  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-br 5087

This theorem is referenced by:  eqbrtrri  5109  3brtr4i  5116  0sdom1dom  9149  1sdom2dom  9157  infxpenc2  9935  dju1p1e2  10087  pwsdompw  10116  r1om  10156  aleph1  10485  canthp1lem1  10566  halflt1  12385  3halfnz  12599  declei  12671  numlti  12672  sqlecan  14162  discr  14193  faclbnd3  14245  hashunlei  14378  hashge2el2dif  14433  geo2lim  15831  0.999...  15837  geoihalfsum  15838  cos2bnd  16146  sin4lt0  16153  eirrlem  16162  rpnnen2lem3  16174  rpnnen2lem9  16180  aleph1re  16203  1nprm  16639  strle2  17120  strle3  17121  1strstr  17184  2strstr  17188  rngstr  17252  srngstr  17263  lmodstr  17279  ipsstr  17290  phlstr  17300  topgrpstr  17315  otpsstr  17330  odrngstr  17357  imasvalstr  17405  chnub  18579  0frgp  19745  cnfldstr  21346  cnfldstrOLD  21361  iscmet3lem3  25267  mbfimaopnlem  25632  mbfsup  25641  mbfi1fseqlem6  25697  aalioulem3  26311  aaliou3lem3  26321  dvradcnv  26399  logi  26564  asin1  26871  log2cnv  26921  log2tlbnd  26922  mule1  27125  bposlem5  27265  bposlem8  27268  zabsle1  27273  trkgstr  28526  0pth  30210  ex-fl  30532  blocnilem  30890  norm3difi  31233  norm3adifii  31234  bcsiALT  31265  nmopsetn0  31951  nmfnsetn0  31964  nmopge0  31997  nmfnge0  32013  0bdop  32079  nmcexi  32112  opsqrlem6  32231  dp2lt10  32958  dplti  32979  dpmul4  32988  idlsrgstr  33577  locfinref  34001  dya2iocct  34440  signswch  34721  hgt750lem  34811  hgt750lem2  34812  subfaclim  35386  faclim  35944  cnndvlem1  36813  taupilem2  37652  cntotbnd  38131  60gcd7e1  42458  3lexlogpow5ineq1  42507  aks4d1p1p7  42527  acos1half  42804  diophren  43259  algstr  43619  pr2dom  43972  tr3dom  43973  binomcxplemnn0  44794  binomcxplemrat  44795  stirlinglem1  46520  dirkercncflem1  46549  fouriersw  46677  meaiunlelem  46914  nthrucw  47332  ceilhalf1  47798  nfermltl2rev  48231  evengpoap3  48287  exple2lt6  48852  nnlog2ge0lt1  49054  catbas  49713  cathomfval  49714  catcofval  49715