Theorem eqbrtri 5091

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

Syntax hints:   = wceq 1539   class class class wbr 5070

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-br 5071

This theorem is referenced by:  eqbrtrri  5093  3brtr4i  5100  infxpenc2  9709  dju1p1e2  9860  pwsdompw  9891  r1om  9931  aleph1  10258  canthp1lem1  10339  neg1lt0  12020  halflt1  12121  3halfnz  12329  declei  12402  numlti  12403  sqlecan  13853  discr  13883  faclbnd3  13934  hashunlei  14068  hashge2el2dif  14122  geo2lim  15515  0.999...  15521  geoihalfsum  15522  cos2bnd  15825  sin4lt0  15832  eirrlem  15841  rpnnen2lem3  15853  rpnnen2lem9  15859  aleph1re  15882  1nprm  16312  strle2  16788  strle3  16789  1strstr  16855  2strstr  16860  2strstr1  16863  rngstr  16934  srngstr  16945  lmodstr  16961  ipsstr  16971  phlstr  16981  topgrpstr  16995  otpsstr  17009  odrngstr  17032  imasvalstr  17079  0frgp  19300  cnfldstr  20512  zlmlemOLD  20631  tnglemOLD  23703  iscmet3lem3  24359  mbfimaopnlem  24724  mbfsup  24733  mbfi1fseqlem6  24790  aalioulem3  25399  aaliou3lem3  25409  dvradcnv  25485  asin1  25949  log2cnv  25999  log2tlbnd  26000  mule1  26202  bposlem5  26341  bposlem8  26344  zabsle1  26349  trkgstr  26709  0pth  28390  ex-fl  28712  blocnilem  29067  norm3difi  29410  norm3adifii  29411  bcsiALT  29442  nmopsetn0  30128  nmfnsetn0  30141  nmopge0  30174  nmfnge0  30190  0bdop  30256  nmcexi  30289  opsqrlem6  30408  dp2lt10  31060  dplti  31081  dpmul4  31090  idlsrgstr  31549  locfinref  31693  dya2iocct  32147  signswch  32440  hgt750lem  32531  hgt750lem2  32532  subfaclim  33050  logi  33606  faclim  33618  cnndvlem1  34644  taupilem2  35420  cntotbnd  35881  60gcd7e1  39941  3lexlogpow5ineq1  39990  aks4d1p1p7  40010  acos1half  40098  diophren  40551  algstr  40918  pr2dom  41032  tr3dom  41033  binomcxplemnn0  41856  binomcxplemrat  41857  stirlinglem1  43505  dirkercncflem1  43534  fouriersw  43662  meaiunlelem  43896  nfermltl2rev  45083  evengpoap3  45139  exple2lt6  45588  nnlog2ge0lt1  45800