Theorem eqbrtri 5116

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

Syntax hints:   = wceq 1540   class class class wbr 5095

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 2701

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 2708  df-cleq 2721  df-clel 2803  df-rab 3397  df-v 3440  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-br 5096

This theorem is referenced by:  eqbrtrri  5118  3brtr4i  5125  0sdom1dom  9145  1sdom2dom  9153  infxpenc2  9935  dju1p1e2  10087  pwsdompw  10116  r1om  10156  aleph1  10484  canthp1lem1  10565  halflt1  12359  3halfnz  12573  declei  12645  numlti  12646  sqlecan  14134  discr  14165  faclbnd3  14217  hashunlei  14350  hashge2el2dif  14405  geo2lim  15800  0.999...  15806  geoihalfsum  15807  cos2bnd  16115  sin4lt0  16122  eirrlem  16131  rpnnen2lem3  16143  rpnnen2lem9  16149  aleph1re  16172  1nprm  16608  strle2  17088  strle3  17089  1strstr  17152  2strstr  17156  rngstr  17220  srngstr  17231  lmodstr  17247  ipsstr  17258  phlstr  17268  topgrpstr  17283  otpsstr  17298  odrngstr  17325  imasvalstr  17373  0frgp  19676  cnfldstr  21281  cnfldstrOLD  21296  iscmet3lem3  25206  mbfimaopnlem  25572  mbfsup  25581  mbfi1fseqlem6  25637  aalioulem3  26258  aaliou3lem3  26268  dvradcnv  26346  logi  26512  asin1  26820  log2cnv  26870  log2tlbnd  26871  mule1  27074  bposlem5  27215  bposlem8  27218  zabsle1  27223  trkgstr  28407  0pth  30087  ex-fl  30409  blocnilem  30766  norm3difi  31109  norm3adifii  31110  bcsiALT  31141  nmopsetn0  31827  nmfnsetn0  31840  nmopge0  31873  nmfnge0  31889  0bdop  31955  nmcexi  31988  opsqrlem6  32107  dp2lt10  32837  dplti  32858  dpmul4  32867  chnub  32967  idlsrgstr  33452  locfinref  33810  dya2iocct  34250  signswch  34531  hgt750lem  34621  hgt750lem2  34622  subfaclim  35163  faclim  35721  cnndvlem1  36513  taupilem2  37298  cntotbnd  37778  60gcd7e1  41981  3lexlogpow5ineq1  42030  aks4d1p1p7  42050  acos1half  42334  diophren  42789  algstr  43149  pr2dom  43503  tr3dom  43504  binomcxplemnn0  44325  binomcxplemrat  44326  stirlinglem1  46059  dirkercncflem1  46088  fouriersw  46216  meaiunlelem  46453  ceilhalf1  47322  nfermltl2rev  47731  evengpoap3  47787  exple2lt6  48352  nnlog2ge0lt1  48555  catbas  49215  cathomfval  49216  catcofval  49217