Theorem eqbrtri 5096

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

Syntax hints:   = wceq 1539   class class class wbr 5075

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 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-rab 3074  df-v 3435  df-dif 3891  df-un 3893  df-nul 4258  df-if 4461  df-sn 4563  df-pr 4565  df-op 4569  df-br 5076

This theorem is referenced by:  eqbrtrri  5098  3brtr4i  5105  infxpenc2  9787  dju1p1e2  9938  pwsdompw  9969  r1om  10009  aleph1  10336  canthp1lem1  10417  neg1lt0  12099  halflt1  12200  3halfnz  12408  declei  12482  numlti  12483  sqlecan  13934  discr  13964  faclbnd3  14015  hashunlei  14149  hashge2el2dif  14203  geo2lim  15596  0.999...  15602  geoihalfsum  15603  cos2bnd  15906  sin4lt0  15913  eirrlem  15922  rpnnen2lem3  15934  rpnnen2lem9  15940  aleph1re  15963  1nprm  16393  strle2  16869  strle3  16870  1strstr  16936  1strstr1  16937  2strstr  16943  2strstr1  16946  rngstr  17017  srngstr  17028  lmodstr  17044  ipsstr  17055  phlstr  17065  topgrpstr  17080  otpsstr  17095  odrngstr  17122  imasvalstr  17171  0frgp  19394  cnfldstr  20608  zlmlemOLD  20728  tnglemOLD  23806  iscmet3lem3  24463  mbfimaopnlem  24828  mbfsup  24837  mbfi1fseqlem6  24894  aalioulem3  25503  aaliou3lem3  25513  dvradcnv  25589  asin1  26053  log2cnv  26103  log2tlbnd  26104  mule1  26306  bposlem5  26445  bposlem8  26448  zabsle1  26453  trkgstr  26814  0pth  28498  ex-fl  28820  blocnilem  29175  norm3difi  29518  norm3adifii  29519  bcsiALT  29550  nmopsetn0  30236  nmfnsetn0  30249  nmopge0  30282  nmfnge0  30298  0bdop  30364  nmcexi  30397  opsqrlem6  30516  dp2lt10  31167  dplti  31188  dpmul4  31197  idlsrgstr  31656  locfinref  31800  dya2iocct  32256  signswch  32549  hgt750lem  32640  hgt750lem2  32641  subfaclim  33159  logi  33709  faclim  33721  cnndvlem1  34726  taupilem2  35502  cntotbnd  35963  60gcd7e1  40020  3lexlogpow5ineq1  40069  aks4d1p1p7  40089  acos1half  40177  diophren  40642  algstr  41009  pr2dom  41141  tr3dom  41142  binomcxplemnn0  41974  binomcxplemrat  41975  stirlinglem1  43622  dirkercncflem1  43651  fouriersw  43779  meaiunlelem  44013  nfermltl2rev  45206  evengpoap3  45262  exple2lt6  45711  nnlog2ge0lt1  45923