Theorem eqbrtri 5133

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

Syntax hints:   = wceq 1570   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 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-v 3457  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4288  df-if 4489  df-sn 4591  df-pr 4593  df-op 4597  df-br 5111

This theorem is referenced by:  eqbrtrri  5135  3brtr4i  5142  0sdom1dom  9207  1sdom2dom  9215  infxpenc2  10007  dju1p1e2  10158  pwsdompw  10187  r1om  10227  aleph1  10557  canthp1lem1  10638  halflt1  12462  3halfnz  12676  declei  12753  numlti  12754  sqlecan  14247  discr  14278  faclbnd3  14330  hashunlei  14464  hashge2el2dif  14519  geo2lim  15931  0.999...  15937  geoihalfsum  15938  cos2bnd  16245  sin4lt0  16252  eirrlem  16261  rpnnen2lem3  16273  rpnnen2lem9  16279  aleph1re  16302  1nprm  16738  strle2  17220  strle3  17221  1strstr  17284  2strstr  17288  rngstr  17352  srngstr  17363  lmodstr  17379  ipsstr  17390  phlstr  17400  topgrpstr  17415  otpsstr  17430  odrngstr  17457  imasvalstr  17505  chnub  18679  0frgp  19850  cnfldstr  21505  iscmet3lem3  25430  mbfimaopnlem  25795  mbfsup  25804  mbfi1fseqlem6  25860  aalioulem3  26478  aaliou3lem3  26488  dvradcnv  26565  logi  26733  asin1  27040  log2cnv  27090  log2tlbnd  27091  mule1  27293  bposlem5  27433  bposlem8  27436  zabsle1  27441  trkgstr  28694  0pth  30457  ex-fl  30779  blocnilem  31137  norm3difi  31480  norm3adifii  31481  bcsiALT  31512  nmopsetn0  32198  nmfnsetn0  32211  nmopge0  32244  nmfnge0  32260  0bdop  32326  nmcexi  32359  opsqrlem6  32478  dp2lt10  33184  dplti  33205  dpmul4  33214  idlsrgstr  33773  locfinref  34212  dya2iocct  34651  signswch  34929  hgt750lem  35019  hgt750lem2  35020  subfaclim  35661  faclim  36219  cnndvlem1  37107  taupilem2  37947  cntotbnd  38428  60gcd7e1  42753  3lexlogpow5ineq1  42802  aks4d1p1p7  42822  acos1half  43100  diophren  43523  algstr  43883  pr2dom  44236  tr3dom  44237  binomcxplemnn0  45042  binomcxplemrat  45043  stirlinglem1  46771  dirkercncflem1  46800  fouriersw  46928  meaiunlelem  47165  nthrucw  47590  ceilhalf1  48058  nfermltl2rev  48491  evengpoap3  48547  exple2lt6  49127  nnlog2ge0lt1  49329  catbas  49987  cathomfval  49988  catcofval  49989