Theorem eqbrtri 5119

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

Syntax hints:   = wceq 1541   class class class wbr 5098

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 2708

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 2715  df-cleq 2728  df-clel 2811  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-br 5099

This theorem is referenced by:  eqbrtrri  5121  3brtr4i  5128  0sdom1dom  9146  1sdom2dom  9154  infxpenc2  9932  dju1p1e2  10084  pwsdompw  10113  r1om  10153  aleph1  10482  canthp1lem1  10563  halflt1  12358  3halfnz  12571  declei  12643  numlti  12644  sqlecan  14132  discr  14163  faclbnd3  14215  hashunlei  14348  hashge2el2dif  14403  geo2lim  15798  0.999...  15804  geoihalfsum  15805  cos2bnd  16113  sin4lt0  16120  eirrlem  16129  rpnnen2lem3  16141  rpnnen2lem9  16147  aleph1re  16170  1nprm  16606  strle2  17086  strle3  17087  1strstr  17150  2strstr  17154  rngstr  17218  srngstr  17229  lmodstr  17245  ipsstr  17256  phlstr  17266  topgrpstr  17281  otpsstr  17296  odrngstr  17323  imasvalstr  17371  chnub  18545  0frgp  19708  cnfldstr  21311  cnfldstrOLD  21326  iscmet3lem3  25246  mbfimaopnlem  25612  mbfsup  25621  mbfi1fseqlem6  25677  aalioulem3  26298  aaliou3lem3  26308  dvradcnv  26386  logi  26552  asin1  26860  log2cnv  26910  log2tlbnd  26911  mule1  27114  bposlem5  27255  bposlem8  27258  zabsle1  27263  trkgstr  28516  0pth  30200  ex-fl  30522  blocnilem  30879  norm3difi  31222  norm3adifii  31223  bcsiALT  31254  nmopsetn0  31940  nmfnsetn0  31953  nmopge0  31986  nmfnge0  32002  0bdop  32068  nmcexi  32101  opsqrlem6  32220  dp2lt10  32965  dplti  32986  dpmul4  32995  idlsrgstr  33583  locfinref  33998  dya2iocct  34437  signswch  34718  hgt750lem  34808  hgt750lem2  34809  subfaclim  35382  faclim  35940  cnndvlem1  36737  taupilem2  37527  cntotbnd  37997  60gcd7e1  42259  3lexlogpow5ineq1  42308  aks4d1p1p7  42328  acos1half  42613  diophren  43055  algstr  43415  pr2dom  43768  tr3dom  43769  binomcxplemnn0  44590  binomcxplemrat  44591  stirlinglem1  46318  dirkercncflem1  46347  fouriersw  46475  meaiunlelem  46712  nthrucw  47130  ceilhalf1  47580  nfermltl2rev  47989  evengpoap3  48045  exple2lt6  48610  nnlog2ge0lt1  48812  catbas  49471  cathomfval  49472  catcofval  49473