Theorem eqbrtri 5116

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

Syntax hints:   = wceq 1541   class class class wbr 5095

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-rab 3397  df-v 3439  df-dif 3901  df-un 3903  df-ss 3915  df-nul 4283  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-br 5096

This theorem is referenced by:  eqbrtrri  5118  3brtr4i  5125  0sdom1dom  9139  1sdom2dom  9147  infxpenc2  9922  dju1p1e2  10074  pwsdompw  10103  r1om  10143  aleph1  10471  canthp1lem1  10552  halflt1  12347  3halfnz  12560  declei  12632  numlti  12633  sqlecan  14120  discr  14151  faclbnd3  14203  hashunlei  14336  hashge2el2dif  14391  geo2lim  15786  0.999...  15792  geoihalfsum  15793  cos2bnd  16101  sin4lt0  16108  eirrlem  16117  rpnnen2lem3  16129  rpnnen2lem9  16135  aleph1re  16158  1nprm  16594  strle2  17074  strle3  17075  1strstr  17138  2strstr  17142  rngstr  17206  srngstr  17217  lmodstr  17233  ipsstr  17244  phlstr  17254  topgrpstr  17269  otpsstr  17284  odrngstr  17311  imasvalstr  17359  chnub  18532  0frgp  19695  cnfldstr  21297  cnfldstrOLD  21312  iscmet3lem3  25220  mbfimaopnlem  25586  mbfsup  25595  mbfi1fseqlem6  25651  aalioulem3  26272  aaliou3lem3  26282  dvradcnv  26360  logi  26526  asin1  26834  log2cnv  26884  log2tlbnd  26885  mule1  27088  bposlem5  27229  bposlem8  27232  zabsle1  27237  trkgstr  28425  0pth  30109  ex-fl  30431  blocnilem  30788  norm3difi  31131  norm3adifii  31132  bcsiALT  31163  nmopsetn0  31849  nmfnsetn0  31862  nmopge0  31895  nmfnge0  31911  0bdop  31977  nmcexi  32010  opsqrlem6  32129  dp2lt10  32873  dplti  32894  dpmul4  32903  idlsrgstr  33476  locfinref  33877  dya2iocct  34316  signswch  34597  hgt750lem  34687  hgt750lem2  34688  subfaclim  35255  faclim  35813  cnndvlem1  36604  taupilem2  37389  cntotbnd  37859  60gcd7e1  42121  3lexlogpow5ineq1  42170  aks4d1p1p7  42190  acos1half  42479  diophren  42933  algstr  43293  pr2dom  43647  tr3dom  43648  binomcxplemnn0  44469  binomcxplemrat  44470  stirlinglem1  46199  dirkercncflem1  46228  fouriersw  46356  meaiunlelem  46593  nthrucw  47011  ceilhalf1  47461  nfermltl2rev  47870  evengpoap3  47926  exple2lt6  48491  nnlog2ge0lt1  48694  catbas  49354  cathomfval  49355  catcofval  49356