Theorem eqbrtri 5163

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

Syntax hints:   = wceq 1539   class class class wbr 5142

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-sb 2064  df-clab 2714  df-cleq 2728  df-clel 2815  df-rab 3436  df-v 3481  df-dif 3953  df-un 3955  df-ss 3967  df-nul 4333  df-if 4525  df-sn 4626  df-pr 4628  df-op 4632  df-br 5143

This theorem is referenced by:  eqbrtrri  5165  3brtr4i  5172  0sdom1dom  9275  1sdom2dom  9284  infxpenc2  10063  dju1p1e2  10215  pwsdompw  10244  r1om  10284  aleph1  10612  canthp1lem1  10693  neg1lt0  12384  halflt1  12485  3halfnz  12699  declei  12771  numlti  12772  sqlecan  14249  discr  14280  faclbnd3  14332  hashunlei  14465  hashge2el2dif  14520  geo2lim  15912  0.999...  15918  geoihalfsum  15919  cos2bnd  16225  sin4lt0  16232  eirrlem  16241  rpnnen2lem3  16253  rpnnen2lem9  16259  aleph1re  16282  1nprm  16717  strle2  17197  strle3  17198  1strstr  17262  1strstr1  17263  2strstr  17268  2strstr1  17271  rngstr  17343  srngstr  17354  lmodstr  17370  ipsstr  17381  phlstr  17391  topgrpstr  17406  otpsstr  17421  odrngstr  17448  imasvalstr  17497  0frgp  19798  cnfldstr  21367  cnfldstrOLD  21382  zlmlemOLD  21529  tnglemOLD  24655  iscmet3lem3  25325  mbfimaopnlem  25691  mbfsup  25700  mbfi1fseqlem6  25756  aalioulem3  26377  aaliou3lem3  26387  dvradcnv  26465  logi  26630  asin1  26938  log2cnv  26988  log2tlbnd  26989  mule1  27192  bposlem5  27333  bposlem8  27336  zabsle1  27341  trkgstr  28453  0pth  30145  ex-fl  30467  blocnilem  30824  norm3difi  31167  norm3adifii  31168  bcsiALT  31199  nmopsetn0  31885  nmfnsetn0  31898  nmopge0  31931  nmfnge0  31947  0bdop  32013  nmcexi  32046  opsqrlem6  32165  dp2lt10  32867  dplti  32888  dpmul4  32897  chnub  33003  idlsrgstr  33531  locfinref  33841  dya2iocct  34283  signswch  34577  hgt750lem  34667  hgt750lem2  34668  subfaclim  35194  faclim  35747  cnndvlem1  36539  taupilem2  37324  cntotbnd  37804  60gcd7e1  42007  3lexlogpow5ineq1  42056  aks4d1p1p7  42076  acos1half  42393  diophren  42829  algstr  43190  pr2dom  43545  tr3dom  43546  binomcxplemnn0  44373  binomcxplemrat  44374  stirlinglem1  46094  dirkercncflem1  46123  fouriersw  46251  meaiunlelem  46488  nfermltl2rev  47735  evengpoap3  47791  exple2lt6  48285  nnlog2ge0lt1  48492