Theorem eqbrtri 5130

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

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

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 2734

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 2741  df-cleq 2754  df-clel 2837  df-rab 3415  df-v 3455  df-dif 3905  df-un 3907  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-br 5108

This theorem is used by:  eqbrtrri  5132  3brtr4i  5139  0sdom1dom  9220  1sdom2dom  9228  infxpenc2  10029  dju1p1e2  10180  pwsdompw  10209  r1om  10249  aleph1  10584  canthp1lem1  10665  halflt1  12489  3halfnz  12704  declei  12781  numlti  12782  sqlecan  14277  discr  14308  faclbnd3  14360  hashunlei  14494  hashge2el2dif  14549  geo2lim  15968  0.999...  15974  geoihalfsum  15975  cos2bnd  16282  sin4lt0  16289  eirrlem  16298  rpnnen2lem3  16310  rpnnen2lem9  16316  aleph1re  16339  1nprm  16775  strle2  17257  strle3  17258  1strstr  17321  2strstr  17325  rngstr  17389  srngstr  17400  lmodstr  17416  ipsstr  17427  phlstr  17437  topgrpstr  17452  otpsstr  17467  odrngstr  17494  imasvalstr  17542  chnub  18716  0frgp  19912  cnfldstr  21593  iscmet3lem3  25524  mbfimaopnlem  25889  mbfsup  25898  mbfi1fseqlem6  25954  aalioulem3  26577  aaliou3lem3  26587  dvradcnv  26664  logi  26832  asin1  27139  log2cnv  27189  log2tlbnd  27190  mule1  27392  bposlem5  27532  bposlem8  27535  zabsle1  27540  trkgstr  28793  0pth  30603  ex-fl  30935  blocnilem  31293  norm3difi  31636  norm3adifii  31637  bcsiALT  31668  nmopsetn0  32354  nmfnsetn0  32367  nmopge0  32400  nmfnge0  32416  0bdop  32482  nmcexi  32515  opsqrlem6  32634  dp2lt10  33337  dplti  33358  dpmul4  33367  idlsrgstr  33920  locfinref  34359  dya2iocct  34799  signswch  35077  hgt750lem  35167  hgt750lem2  35168  subfaclim  35775  faclim  36333  cnndvlem1  37242  taupilem2  38082  cntotbnd  38554  60gcd7e1  42879  3lexlogpow5ineq1  42928  aks4d1p1p7  42948  acos1half  43241  diophren  43662  algstr  44022  pr2dom  44375  tr3dom  44376  binomcxplemnn0  45181  binomcxplemrat  45182  stirlinglem1  46910  dirkercncflem1  46939  fouriersw  47067  meaiunlelem  47304  numtowerdt  47742  ceilhalf1  48234  nfermltl2rev  48667  evengpoap3  48723  exple2lt6  49302  nnlog2ge0lt1  49504  catbas  50160  cathomfval  50161  catcofval  50162