Theorem eqbrtri 5169

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

Syntax hints:   = wceq 1537   class class class wbr 5148

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-rab 3434  df-v 3480  df-dif 3966  df-un 3968  df-ss 3980  df-nul 4340  df-if 4532  df-sn 4632  df-pr 4634  df-op 4638  df-br 5149

This theorem is referenced by:  eqbrtrri  5171  3brtr4i  5178  0sdom1dom  9272  1sdom2dom  9281  infxpenc2  10060  dju1p1e2  10212  pwsdompw  10241  r1om  10281  aleph1  10609  canthp1lem1  10690  neg1lt0  12381  halflt1  12482  3halfnz  12695  declei  12767  numlti  12768  sqlecan  14245  discr  14276  faclbnd3  14328  hashunlei  14461  hashge2el2dif  14516  geo2lim  15908  0.999...  15914  geoihalfsum  15915  cos2bnd  16221  sin4lt0  16228  eirrlem  16237  rpnnen2lem3  16249  rpnnen2lem9  16255  aleph1re  16278  1nprm  16713  strle2  17193  strle3  17194  1strstr  17260  1strstr1  17261  2strstr  17267  2strstr1  17270  rngstr  17344  srngstr  17355  lmodstr  17371  ipsstr  17382  phlstr  17392  topgrpstr  17407  otpsstr  17422  odrngstr  17449  imasvalstr  17498  0frgp  19812  cnfldstr  21384  cnfldstrOLD  21399  zlmlemOLD  21546  tnglemOLD  24670  iscmet3lem3  25338  mbfimaopnlem  25704  mbfsup  25713  mbfi1fseqlem6  25770  aalioulem3  26391  aaliou3lem3  26401  dvradcnv  26479  logi  26644  asin1  26952  log2cnv  27002  log2tlbnd  27003  mule1  27206  bposlem5  27347  bposlem8  27350  zabsle1  27355  trkgstr  28467  0pth  30154  ex-fl  30476  blocnilem  30833  norm3difi  31176  norm3adifii  31177  bcsiALT  31208  nmopsetn0  31894  nmfnsetn0  31907  nmopge0  31940  nmfnge0  31956  0bdop  32022  nmcexi  32055  opsqrlem6  32174  dp2lt10  32851  dplti  32872  dpmul4  32881  chnub  32986  idlsrgstr  33510  locfinref  33802  dya2iocct  34262  signswch  34555  hgt750lem  34645  hgt750lem2  34646  subfaclim  35173  faclim  35726  cnndvlem1  36520  taupilem2  37305  cntotbnd  37783  60gcd7e1  41987  3lexlogpow5ineq1  42036  aks4d1p1p7  42056  acos1half  42367  diophren  42801  algstr  43162  pr2dom  43517  tr3dom  43518  binomcxplemnn0  44345  binomcxplemrat  44346  stirlinglem1  46030  dirkercncflem1  46059  fouriersw  46187  meaiunlelem  46424  nfermltl2rev  47668  evengpoap3  47724  exple2lt6  48209  nnlog2ge0lt1  48416