Theorem eqbrtri 5131

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

Syntax hints:   = wceq 1541   class class class wbr 5110

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-rab 3406  df-v 3448  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4288  df-if 4492  df-sn 4592  df-pr 4594  df-op 4598  df-br 5111

This theorem is referenced by:  eqbrtrri  5133  3brtr4i  5140  0sdom1dom  9189  1sdom2dom  9198  infxpenc2  9967  dju1p1e2  10118  pwsdompw  10149  r1om  10189  aleph1  10516  canthp1lem1  10597  neg1lt0  12279  halflt1  12380  3halfnz  12591  declei  12663  numlti  12664  sqlecan  14123  discr  14153  faclbnd3  14202  hashunlei  14335  hashge2el2dif  14391  geo2lim  15771  0.999...  15777  geoihalfsum  15778  cos2bnd  16081  sin4lt0  16088  eirrlem  16097  rpnnen2lem3  16109  rpnnen2lem9  16115  aleph1re  16138  1nprm  16566  strle2  17042  strle3  17043  1strstr  17109  1strstr1  17110  2strstr  17116  2strstr1  17119  rngstr  17193  srngstr  17204  lmodstr  17220  ipsstr  17231  phlstr  17241  topgrpstr  17256  otpsstr  17271  odrngstr  17298  imasvalstr  17347  0frgp  19575  cnfldstr  20835  zlmlemOLD  20955  tnglemOLD  24034  iscmet3lem3  24691  mbfimaopnlem  25056  mbfsup  25065  mbfi1fseqlem6  25122  aalioulem3  25731  aaliou3lem3  25741  dvradcnv  25817  asin1  26281  log2cnv  26331  log2tlbnd  26332  mule1  26534  bposlem5  26673  bposlem8  26676  zabsle1  26681  trkgstr  27449  0pth  29132  ex-fl  29454  blocnilem  29809  norm3difi  30152  norm3adifii  30153  bcsiALT  30184  nmopsetn0  30870  nmfnsetn0  30883  nmopge0  30916  nmfnge0  30932  0bdop  30998  nmcexi  31031  opsqrlem6  31150  dp2lt10  31810  dplti  31831  dpmul4  31840  idlsrgstr  32320  locfinref  32511  dya2iocct  32969  signswch  33262  hgt750lem  33353  hgt750lem2  33354  subfaclim  33869  logi  34393  faclim  34405  cnndvlem1  35076  taupilem2  35866  cntotbnd  36328  60gcd7e1  40535  3lexlogpow5ineq1  40584  aks4d1p1p7  40604  acos1half  40695  diophren  41194  algstr  41562  pr2dom  41921  tr3dom  41922  binomcxplemnn0  42751  binomcxplemrat  42752  stirlinglem1  44435  dirkercncflem1  44464  fouriersw  44592  meaiunlelem  44829  nfermltl2rev  46055  evengpoap3  46111  exple2lt6  46560  nnlog2ge0lt1  46772