Theorem eqbrtri 5126

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

This proof depends on syntax axioms:   = wceq 1570   class class class wbr 5103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5104

This theorem is used by:  eqbrtrri  5128  3brtr4i  5135  0sdom1dom  9221  1sdom2dom  9229  infxpenc2  10082  dju1p1e2  10233  pwsdompw  10262  aleph1  10637  canthp1lem1  10718  hfomALT  10842  halflt1  12544  3halfnz  12759  declei  12836  numlti  12837  sqlecan  14333  discr  14364  faclbnd3  14416  hashunlei  14550  hashge2el2dif  14605  geo2lim  16024  0.999...  16030  geoihalfsum  16031  cos2bnd  16336  sin4lt0  16343  eirrlem  16352  rpnnen2lem3  16364  rpnnen2lem9  16370  aleph1re  16393  1nprm  16834  strle2  17317  strle3  17318  1strstr  17381  2strstr  17385  rngstr  17449  srngstr  17460  lmodstr  17476  ipsstr  17487  phlstr  17497  topgrpstr  17512  otpsstr  17527  odrngstr  17554  imasvalstr  17602  chnub  18776  0frgp  19973  cnfldstr  21660  iscmet3lem3  25591  mbfimaopnlem  25956  mbfsup  25965  mbfi1fseqlem6  26021  aalioulem3  26643  aaliou3lem3  26653  dvradcnv  26730  logi  26897  asin1  27204  log2cnv  27254  log2tlbnd  27255  mule1  27457  bposlem5  27597  bposlem8  27600  zabsle1  27605  trkgstr  28888  0pth  30698  ex-fl  31030  blocnilem  31388  norm3difi  31731  norm3adifii  31732  bcsiALT  31763  nmopsetn0  32449  nmfnsetn0  32462  nmopge0  32495  nmfnge0  32511  0bdop  32577  nmcexi  32610  opsqrlem6  32729  dp2lt10  33432  dplti  33453  dpmul4  33462  idlsrgstr  34016  locfinref  34455  dya2iocct  34895  signswch  35173  hgt750lem  35263  hgt750lem2  35264  subfaclim  35922  faclim  36480  cnndvlem1  37373  taupilem2  38211  cntotbnd  38698  60gcd7e1  43023  3lexlogpow5ineq1  43072  aks4d1p1p7  43092  acos1half  43377  diophren  43773  algstr  44133  pr2dom  44486  tr3dom  44487  binomcxplemnn0  45292  binomcxplemrat  45293  stirlinglem1  47028  dirkercncflem1  47057  fouriersw  47185  meaiunlelem  47422  numtowerdt  47860  ceilhalf1  48352  nfermltl2rev  48785  evengpoap3  48841  exple2lt6  49420  nnlog2ge0lt1  49622  catbas  50278  cathomfval  50279  catcofval  50280