Theorem eqbrtri 5130

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

This proof depends on syntax axioms:   = wceq 1570   class class class wbr 5106

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-br 5107

This theorem is used by:  eqbrtrri  5132  3brtr4i  5139  0sdom1dom  9268  1sdom2dom  9276  infxpenc2  10131  dju1p1e2  10282  pwsdompw  10311  aleph1  10686  canthp1lem1  10767  hfomALT  10891  halflt1  12593  3halfnz  12808  declei  12885  numlti  12886  sqlecan  14383  discr  14414  faclbnd3  14466  hashunlei  14600  hashge2el2dif  14655  geo2lim  16076  0.999...  16082  geoihalfsum  16083  cos2bnd  16388  sin4lt0  16395  eirrlem  16404  rpnnen2lem3  16416  rpnnen2lem9  16422  aleph1re  16445  1nprm  16886  strle2  17369  strle3  17370  1strstr  17433  2strstr  17437  rngstr  17501  srngstr  17512  lmodstr  17528  ipsstr  17539  phlstr  17549  topgrpstr  17564  otpsstr  17579  odrngstr  17606  imasvalstr  17654  chnub  18828  0frgp  20026  cnfldstr  21713  iscmet3lem3  25644  mbfimaopnlem  26009  mbfsup  26018  mbfi1fseqlem6  26074  aalioulem3  26694  aaliou3lem3  26704  dvradcnv  26781  logi  26948  asin1  27255  log2cnv  27305  log2tlbnd  27306  mule1  27508  bposlem5  27648  bposlem8  27651  zabsle1  27656  trkgstr  28939  0pth  30749  ex-fl  31081  blocnilem  31439  norm3difi  31782  norm3adifii  31783  bcsiALT  31814  nmopsetn0  32500  nmfnsetn0  32513  nmopge0  32546  nmfnge0  32562  0bdop  32628  nmcexi  32661  opsqrlem6  32780  dp2lt10  33523  dplti  33544  dpmul4  33553  idlsrgstr  34118  locfinref  34556  dya2iocct  34995  signswch  35273  hgt750lem  35363  hgt750lem2  35364  subfaclim  36133  faclim  36702  cnndvlem1  37594  taupilem2  38448  cntotbnd  38933  60gcd7e1  43258  3lexlogpow5ineq1  43307  aks4d1p1p7  43327  acos1half  43613  diophren  44024  algstr  44378  pr2dom  44731  tr3dom  44732  binomcxplemnn0  45536  binomcxplemrat  45537  stirlinglem1  47299  dirkercncflem1  47328  fouriersw  47456  meaiunlelem  47693  numtowerdt  48131  ceilhalf1  48623  nfermltl2rev  49056  evengpoap3  49112  exple2lt6  49691  nnlog2ge0lt1  49893  catbas  50563  cathomfval  50564  catcofval  50565