Theorem eqbrtri 4436

Description: Substitution of equal classes into a binary relation. (Contributed by NM, 1-Aug-1999.)

Hypotheses

Ref	Expression
eqbrtr.1	|- A = B
eqbrtr.2	|- B R C

Assertion

Ref	Expression
eqbrtri	|- A R C

Proof of Theorem eqbrtri

Step	Hyp	Ref	Expression
1		eqbrtr.2	. 2 |- B R C
2		eqbrtr.1	. . 3 |- A = B
3	2	breq1i 4423	. 2 |- ( A R C <-> B R C )
4	1, 3	mpbir 214	1 |- A R C

Syntax hints:   = wceq 1455   class class class wbr 4416

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-rab 2758  df-v 3059  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-nul 3744  df-if 3894  df-sn 3981  df-pr 3983  df-op 3987  df-br 4417

This theorem is referenced by:  eqbrtrri  4438  3brtr4i  4445  infxpenc2  8479  pm110.643  8633  pwsdompw  8660  r1om  8700  aleph1  9022  canthp1lem1  9103  pwxpndom2  9116  neg1lt0  10744  halflt1  10860  numlti  11104  sqlecan  12413  discr  12441  faclbnd3  12509  hashunlei  12630  hashge2el2dif  12670  geo2lim  13980  0.999...  13986  geoihalfsum  13987  cos2bnd  14291  sin4lt0  14298  eirrlem  14305  rpnnen2lem3  14318  rpnnen2lem9  14324  aleph1re  14346  1nprm  14678  163prm  15145  631prm  15147  strle2  15271  strle3  15272  1strstr  15275  2strstr  15279  rngstr  15293  srngfn  15301  lmodstr  15310  ipsstr  15317  phlstr  15327  topgrpstr  15335  otpsstr  15342  odrngstr  15353  imasvalstr  15399  ipostr  16448  0frgp  17478  cnfldstr  19021  zlmlem  19137  thlle  19309  tnglem  21697  iscmet3lem3  22309  mbfimaopnlem  22660  mbfsup  22669  mbfi1fseqlem6  22727  aalioulem3  23339  aaliou3lem3  23349  dvradcnv  23425  asin1  23869  log2cnv  23919  log2tlbnd  23920  mule1  24124  bposlem5  24265  bposlem8  24268  trkgstr  24541  0pth  25349  ex-fl  25946  blocnilem  26494  norm3difi  26849  norm3adifii  26850  bcsiALT  26881  nmopsetn0  27567  nmfnsetn0  27580  nmopge0  27613  nmfnge0  27629  0bdop  27695  nmcexi  27728  opsqrlem6  27847  locfinref  28717  dya2iocct  29151  signswch  29499  subfaclim  29960  logi  30419  faclim  30431  taupilem2  31768  cntotbnd  32173  diophren  35701  algstr  36088  binomcxplemnn0  36742  binomcxplemrat  36743  stirlinglem1  37974  dirkercncflem1  38003  fouriersw  38133  meaiunlelem  38344  0pth-av  39841  exple2lt6  40422  3halfnz  40590  nnlog2ge0lt1  40650