Theorem eqbrtri 4706

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

Syntax hints:   = wceq 1523   class class class wbr 4685

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-rab 2950  df-v 3233  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-sn 4211  df-pr 4213  df-op 4217  df-br 4686

This theorem is referenced by:  eqbrtrri  4708  3brtr4i  4715  infxpenc2  8883  pm110.643  9037  pwsdompw  9064  r1om  9104  aleph1  9431  canthp1lem1  9512  pwxpndom2  9525  neg1lt0  11165  halflt1  11288  3halfnz  11494  declei  11580  numlti  11583  sqlecan  13011  discr  13041  faclbnd3  13119  hashunlei  13250  hashge2el2dif  13300  geo2lim  14650  0.999...  14656  0.999...OLD  14657  geoihalfsum  14658  cos2bnd  14962  sin4lt0  14969  eirrlem  14976  rpnnen2lem3  14989  rpnnen2lem9  14995  aleph1re  15018  1nprm  15439  strle2  16021  strle3  16022  1strstr  16026  2strstr  16030  rngstr  16047  srngfn  16055  lmodstr  16064  ipsstr  16071  phlstr  16081  topgrpstr  16089  otpsstr  16098  otpsstrOLD  16102  odrngstr  16113  imasvalstr  16159  0frgp  18238  cnfldstr  19796  zlmlem  19913  tnglem  22491  iscmet3lem3  23134  mbfimaopnlem  23467  mbfsup  23476  mbfi1fseqlem6  23532  aalioulem3  24134  aaliou3lem3  24144  dvradcnv  24220  asin1  24666  log2cnv  24716  log2tlbnd  24717  mule1  24919  bposlem5  25058  bposlem8  25061  zabsle1  25066  trkgstr  25388  0pth  27103  ex-fl  27434  blocnilem  27787  norm3difi  28132  norm3adifii  28133  bcsiALT  28164  nmopsetn0  28852  nmfnsetn0  28865  nmopge0  28898  nmfnge0  28914  0bdop  28980  nmcexi  29013  opsqrlem6  29132  dp2lt10  29719  dplti  29741  dpmul4  29750  locfinref  30036  dya2iocct  30470  signswch  30766  hgt750lem  30857  hgt750lem2  30858  subfaclim  31296  logi  31746  faclim  31758  cnndvlem1  32653  taupilem2  33298  cntotbnd  33725  diophren  37694  algstr  38064  binomcxplemnn0  38865  binomcxplemrat  38866  stirlinglem1  40609  dirkercncflem1  40638  fouriersw  40766  meaiunlelem  41003  evengpoap3  42012  exple2lt6  42470  nnlog2ge0lt1  42685