Theorem eqbrtri 5100

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

Syntax hints:   = wceq 1547   class class class wbr 5079

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-rab 3393  df-v 3434  df-dif 3893  df-un 3895  df-ss 3907  df-nul 4269  df-if 4462  df-sn 4563  df-pr 4565  df-op 4569  df-br 5080

This theorem is referenced by:  eqbrtrri  5102  3brtr4i  5109  0sdom1dom  9153  1sdom2dom  9161  infxpenc2  9942  dju1p1e2  10094  pwsdompw  10123  r1om  10163  aleph1  10492  canthp1lem1  10573  halflt1  12392  3halfnz  12606  declei  12678  numlti  12679  sqlecan  14169  discr  14200  faclbnd3  14252  hashunlei  14385  hashge2el2dif  14440  geo2lim  15838  0.999...  15844  geoihalfsum  15845  cos2bnd  16153  sin4lt0  16160  eirrlem  16169  rpnnen2lem3  16181  rpnnen2lem9  16187  aleph1re  16210  1nprm  16646  strle2  17127  strle3  17128  1strstr  17191  2strstr  17195  rngstr  17259  srngstr  17270  lmodstr  17286  ipsstr  17297  phlstr  17307  topgrpstr  17322  otpsstr  17337  odrngstr  17364  imasvalstr  17412  chnub  18586  0frgp  19752  cnfldstr  21356  iscmet3lem3  25282  mbfimaopnlem  25647  mbfsup  25656  mbfi1fseqlem6  25712  aalioulem3  26325  aaliou3lem3  26335  dvradcnv  26411  logi  26576  asin1  26883  log2cnv  26933  log2tlbnd  26934  mule1  27136  bposlem5  27276  bposlem8  27279  zabsle1  27284  trkgstr  28537  0pth  30220  ex-fl  30542  blocnilem  30900  norm3difi  31243  norm3adifii  31244  bcsiALT  31275  nmopsetn0  31961  nmfnsetn0  31974  nmopge0  32007  nmfnge0  32023  0bdop  32089  nmcexi  32122  opsqrlem6  32241  dp2lt10  32969  dplti  32990  dpmul4  32999  idlsrgstr  33592  locfinref  34032  dya2iocct  34471  signswch  34752  hgt750lem  34842  hgt750lem2  34843  subfaclim  35423  faclim  35981  cnndvlem1  36850  taupilem2  37689  cntotbnd  38170  60gcd7e1  42497  3lexlogpow5ineq1  42546  aks4d1p1p7  42566  acos1half  42842  diophren  43265  algstr  43625  pr2dom  43978  tr3dom  43979  binomcxplemnn0  44800  binomcxplemrat  44801  stirlinglem1  46524  dirkercncflem1  46553  fouriersw  46681  meaiunlelem  46918  nthrucw  47338  ceilhalf1  47808  nfermltl2rev  48241  evengpoap3  48297  exple2lt6  48862  nnlog2ge0lt1  49064  catbas  49723  cathomfval  49724  catcofval  49725