Theorem eqbrtri 5145

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

Syntax hints:   = wceq 1540   class class class wbr 5124

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-rab 3421  df-v 3466  df-dif 3934  df-un 3936  df-ss 3948  df-nul 4314  df-if 4506  df-sn 4607  df-pr 4609  df-op 4613  df-br 5125

This theorem is referenced by:  eqbrtrri  5147  3brtr4i  5154  0sdom1dom  9251  1sdom2dom  9260  infxpenc2  10041  dju1p1e2  10193  pwsdompw  10222  r1om  10262  aleph1  10590  canthp1lem1  10671  neg1lt0  12362  halflt1  12463  3halfnz  12677  declei  12749  numlti  12750  sqlecan  14232  discr  14263  faclbnd3  14315  hashunlei  14448  hashge2el2dif  14503  geo2lim  15896  0.999...  15902  geoihalfsum  15903  cos2bnd  16211  sin4lt0  16218  eirrlem  16227  rpnnen2lem3  16239  rpnnen2lem9  16245  aleph1re  16268  1nprm  16703  strle2  17183  strle3  17184  1strstr  17247  1strstr1  17248  2strstr  17253  rngstr  17317  srngstr  17328  lmodstr  17344  ipsstr  17355  phlstr  17365  topgrpstr  17380  otpsstr  17395  odrngstr  17422  imasvalstr  17470  0frgp  19765  cnfldstr  21322  cnfldstrOLD  21337  iscmet3lem3  25247  mbfimaopnlem  25613  mbfsup  25622  mbfi1fseqlem6  25678  aalioulem3  26299  aaliou3lem3  26309  dvradcnv  26387  logi  26553  asin1  26861  log2cnv  26911  log2tlbnd  26912  mule1  27115  bposlem5  27256  bposlem8  27259  zabsle1  27264  trkgstr  28428  0pth  30111  ex-fl  30433  blocnilem  30790  norm3difi  31133  norm3adifii  31134  bcsiALT  31165  nmopsetn0  31851  nmfnsetn0  31864  nmopge0  31897  nmfnge0  31913  0bdop  31979  nmcexi  32012  opsqrlem6  32131  dp2lt10  32863  dplti  32884  dpmul4  32893  chnub  32997  idlsrgstr  33522  locfinref  33877  dya2iocct  34317  signswch  34598  hgt750lem  34688  hgt750lem2  34689  subfaclim  35215  faclim  35768  cnndvlem1  36560  taupilem2  37345  cntotbnd  37825  60gcd7e1  42023  3lexlogpow5ineq1  42072  aks4d1p1p7  42092  acos1half  42376  diophren  42811  algstr  43172  pr2dom  43526  tr3dom  43527  binomcxplemnn0  44348  binomcxplemrat  44349  stirlinglem1  46083  dirkercncflem1  46112  fouriersw  46240  meaiunlelem  46477  ceilhalf1  47343  nfermltl2rev  47737  evengpoap3  47793  exple2lt6  48319  nnlog2ge0lt1  48526  catbas  49126  cathomfval  49127  catcofval  49128