Theorem eqbrtri 5170

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

Syntax hints:   = wceq 1542   class class class wbr 5149

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-br 5150

This theorem is referenced by:  eqbrtrri  5172  3brtr4i  5179  0sdom1dom  9238  1sdom2dom  9247  infxpenc2  10017  dju1p1e2  10168  pwsdompw  10199  r1om  10239  aleph1  10566  canthp1lem1  10647  neg1lt0  12329  halflt1  12430  3halfnz  12641  declei  12713  numlti  12714  sqlecan  14173  discr  14203  faclbnd3  14252  hashunlei  14385  hashge2el2dif  14441  geo2lim  15821  0.999...  15827  geoihalfsum  15828  cos2bnd  16131  sin4lt0  16138  eirrlem  16147  rpnnen2lem3  16159  rpnnen2lem9  16165  aleph1re  16188  1nprm  16616  strle2  17092  strle3  17093  1strstr  17159  1strstr1  17160  2strstr  17166  2strstr1  17169  rngstr  17243  srngstr  17254  lmodstr  17270  ipsstr  17281  phlstr  17291  topgrpstr  17306  otpsstr  17321  odrngstr  17348  imasvalstr  17397  0frgp  19647  cnfldstr  20946  zlmlemOLD  21067  tnglemOLD  24150  iscmet3lem3  24807  mbfimaopnlem  25172  mbfsup  25181  mbfi1fseqlem6  25238  aalioulem3  25847  aaliou3lem3  25857  dvradcnv  25933  asin1  26399  log2cnv  26449  log2tlbnd  26450  mule1  26652  bposlem5  26791  bposlem8  26794  zabsle1  26799  trkgstr  27726  0pth  29409  ex-fl  29731  blocnilem  30088  norm3difi  30431  norm3adifii  30432  bcsiALT  30463  nmopsetn0  31149  nmfnsetn0  31162  nmopge0  31195  nmfnge0  31211  0bdop  31277  nmcexi  31310  opsqrlem6  31429  dp2lt10  32081  dplti  32102  dpmul4  32111  idlsrgstr  32647  locfinref  32852  dya2iocct  33310  signswch  33603  hgt750lem  33694  hgt750lem2  33695  subfaclim  34210  logi  34735  faclim  34747  gg-cnfldstr  35219  cnndvlem1  35461  taupilem2  36251  cntotbnd  36712  60gcd7e1  40918  3lexlogpow5ineq1  40967  aks4d1p1p7  40987  acos1half  41463  diophren  41599  algstr  41967  pr2dom  42326  tr3dom  42327  binomcxplemnn0  43156  binomcxplemrat  43157  stirlinglem1  44838  dirkercncflem1  44867  fouriersw  44995  meaiunlelem  45232  nfermltl2rev  46459  evengpoap3  46515  exple2lt6  47088  nnlog2ge0lt1  47300