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 230	1 ⊢ 𝐴𝑅𝐶

Syntax hints:   = wceq 1541   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 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

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 2710  df-cleq 2724  df-clel 2810  df-rab 3433  df-v 3476  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-br 5149

This theorem is referenced by:  eqbrtrri  5171  3brtr4i  5178  0sdom1dom  9240  1sdom2dom  9249  infxpenc2  10019  dju1p1e2  10170  pwsdompw  10201  r1om  10241  aleph1  10568  canthp1lem1  10649  neg1lt0  12333  halflt1  12434  3halfnz  12645  declei  12717  numlti  12718  sqlecan  14177  discr  14207  faclbnd3  14256  hashunlei  14389  hashge2el2dif  14445  geo2lim  15825  0.999...  15831  geoihalfsum  15832  cos2bnd  16135  sin4lt0  16142  eirrlem  16151  rpnnen2lem3  16163  rpnnen2lem9  16169  aleph1re  16192  1nprm  16620  strle2  17096  strle3  17097  1strstr  17163  1strstr1  17164  2strstr  17170  2strstr1  17173  rngstr  17247  srngstr  17258  lmodstr  17274  ipsstr  17285  phlstr  17295  topgrpstr  17310  otpsstr  17325  odrngstr  17352  imasvalstr  17401  0frgp  19688  cnfldstr  21146  zlmlemOLD  21286  tnglemOLD  24370  iscmet3lem3  25031  mbfimaopnlem  25396  mbfsup  25405  mbfi1fseqlem6  25462  aalioulem3  26071  aaliou3lem3  26081  dvradcnv  26157  asin1  26623  log2cnv  26673  log2tlbnd  26674  mule1  26876  bposlem5  27015  bposlem8  27018  zabsle1  27023  trkgstr  27950  0pth  29633  ex-fl  29955  blocnilem  30312  norm3difi  30655  norm3adifii  30656  bcsiALT  30687  nmopsetn0  31373  nmfnsetn0  31386  nmopge0  31419  nmfnge0  31435  0bdop  31501  nmcexi  31534  opsqrlem6  31653  dp2lt10  32305  dplti  32326  dpmul4  32335  idlsrgstr  32878  locfinref  33107  dya2iocct  33565  signswch  33858  hgt750lem  33949  hgt750lem2  33950  subfaclim  34465  logi  34996  faclim  35008  gg-cnfldstr  35474  cnndvlem1  35716  taupilem2  36506  cntotbnd  36967  60gcd7e1  41176  3lexlogpow5ineq1  41225  aks4d1p1p7  41245  acos1half  41717  diophren  41853  algstr  42221  pr2dom  42580  tr3dom  42581  binomcxplemnn0  43410  binomcxplemrat  43411  stirlinglem1  45089  dirkercncflem1  45118  fouriersw  45246  meaiunlelem  45483  nfermltl2rev  46710  evengpoap3  46766  exple2lt6  47129  nnlog2ge0lt1  47340