Theorem eqbrtri 5187

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

Syntax hints:   = wceq 1537   class class class wbr 5166

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-br 5167

This theorem is referenced by:  eqbrtrri  5189  3brtr4i  5196  0sdom1dom  9301  1sdom2dom  9310  infxpenc2  10091  dju1p1e2  10243  pwsdompw  10272  r1om  10312  aleph1  10640  canthp1lem1  10721  neg1lt0  12410  halflt1  12511  3halfnz  12722  declei  12794  numlti  12795  sqlecan  14258  discr  14289  faclbnd3  14341  hashunlei  14474  hashge2el2dif  14529  geo2lim  15923  0.999...  15929  geoihalfsum  15930  cos2bnd  16236  sin4lt0  16243  eirrlem  16252  rpnnen2lem3  16264  rpnnen2lem9  16270  aleph1re  16293  1nprm  16726  strle2  17206  strle3  17207  1strstr  17273  1strstr1  17274  2strstr  17280  2strstr1  17283  rngstr  17357  srngstr  17368  lmodstr  17384  ipsstr  17395  phlstr  17405  topgrpstr  17420  otpsstr  17435  odrngstr  17462  imasvalstr  17511  0frgp  19821  cnfldstr  21389  cnfldstrOLD  21404  zlmlemOLD  21551  tnglemOLD  24675  iscmet3lem3  25343  mbfimaopnlem  25709  mbfsup  25718  mbfi1fseqlem6  25775  aalioulem3  26394  aaliou3lem3  26404  dvradcnv  26482  logi  26647  asin1  26955  log2cnv  27005  log2tlbnd  27006  mule1  27209  bposlem5  27350  bposlem8  27353  zabsle1  27358  trkgstr  28470  0pth  30157  ex-fl  30479  blocnilem  30836  norm3difi  31179  norm3adifii  31180  bcsiALT  31211  nmopsetn0  31897  nmfnsetn0  31910  nmopge0  31943  nmfnge0  31959  0bdop  32025  nmcexi  32058  opsqrlem6  32177  dp2lt10  32848  dplti  32869  dpmul4  32878  chnub  32984  idlsrgstr  33495  locfinref  33787  dya2iocct  34245  signswch  34538  hgt750lem  34628  hgt750lem2  34629  subfaclim  35156  faclim  35708  cnndvlem1  36503  taupilem2  37288  cntotbnd  37756  60gcd7e1  41962  3lexlogpow5ineq1  42011  aks4d1p1p7  42031  acos1half  42340  diophren  42769  algstr  43134  pr2dom  43489  tr3dom  43490  binomcxplemnn0  44318  binomcxplemrat  44319  stirlinglem1  45995  dirkercncflem1  46024  fouriersw  46152  meaiunlelem  46389  nfermltl2rev  47617  evengpoap3  47673  exple2lt6  48089  nnlog2ge0lt1  48300