Theorem eqbrtri 5060

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

Syntax hints:   = wceq 1543   class class class wbr 5039

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-sb 2073  df-clab 2715  df-cleq 2728  df-clel 2809  df-rab 3060  df-v 3400  df-dif 3856  df-un 3858  df-nul 4224  df-if 4426  df-sn 4528  df-pr 4530  df-op 4534  df-br 5040

This theorem is referenced by:  eqbrtrri  5062  3brtr4i  5069  infxpenc2  9601  dju1p1e2  9752  pwsdompw  9783  r1om  9823  aleph1  10150  canthp1lem1  10231  neg1lt0  11912  halflt1  12013  3halfnz  12221  declei  12294  numlti  12295  sqlecan  13742  discr  13772  faclbnd3  13823  hashunlei  13957  hashge2el2dif  14011  geo2lim  15402  0.999...  15408  geoihalfsum  15409  cos2bnd  15712  sin4lt0  15719  eirrlem  15728  rpnnen2lem3  15740  rpnnen2lem9  15746  aleph1re  15769  1nprm  16199  strle2  16777  strle3  16778  1strstr  16782  2strstr  16786  rngstr  16803  srngstr  16811  lmodstr  16820  ipsstr  16827  phlstr  16837  topgrpstr  16845  otpsstr  16852  odrngstr  16864  imasvalstr  16910  0frgp  19123  cnfldstr  20319  zlmlem  20437  tnglem  23492  iscmet3lem3  24141  mbfimaopnlem  24506  mbfsup  24515  mbfi1fseqlem6  24572  aalioulem3  25181  aaliou3lem3  25191  dvradcnv  25267  asin1  25731  log2cnv  25781  log2tlbnd  25782  mule1  25984  bposlem5  26123  bposlem8  26126  zabsle1  26131  trkgstr  26489  0pth  28162  ex-fl  28484  blocnilem  28839  norm3difi  29182  norm3adifii  29183  bcsiALT  29214  nmopsetn0  29900  nmfnsetn0  29913  nmopge0  29946  nmfnge0  29962  0bdop  30028  nmcexi  30061  opsqrlem6  30180  dp2lt10  30832  dplti  30853  dpmul4  30862  idlsrgstr  31315  locfinref  31459  dya2iocct  31913  signswch  32206  hgt750lem  32297  hgt750lem2  32298  subfaclim  32817  logi  33369  faclim  33381  cnndvlem1  34403  taupilem2  35176  cntotbnd  35640  60gcd7e1  39696  3lexlogpow5ineq1  39745  aks4d1p1p7  39764  acos1half  39833  diophren  40279  algstr  40646  pr2dom  40760  tr3dom  40761  binomcxplemnn0  41581  binomcxplemrat  41582  stirlinglem1  43233  dirkercncflem1  43262  fouriersw  43390  meaiunlelem  43624  nfermltl2rev  44811  evengpoap3  44867  exple2lt6  45316  nnlog2ge0lt1  45528