Theorem eqbrtri 4332

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 4320	. 2 |- ( A R C <-> B R C )
4	1, 3	mpbir 209	1 |- A R C

Syntax hints:   = wceq 1369   class class class wbr 4313

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-rab 2745  df-v 2995  df-dif 3352  df-un 3354  df-in 3356  df-ss 3363  df-nul 3659  df-if 3813  df-sn 3899  df-pr 3901  df-op 3905  df-br 4314

This theorem is referenced by:  eqbrtrri  4334  3brtr4i  4341  infxpenc2  8209  infxpenc2OLD  8213  pm110.643  8367  pwsdompw  8394  r1om  8434  aleph1  8756  canthp1lem1  8840  pwxpndom2  8853  neg1lt0  10449  halflt1  10564  numlti  10800  sqlecan  11993  discr  12022  faclbnd3  12089  hashunlei  12196  hashge2el2dif  12205  geo2lim  13356  0.999...  13362  geoihalfsum  13363  cos2bnd  13493  sin4lt0  13500  eirrlem  13507  rpnnen2lem3  13520  rpnnen2lem9  13526  aleph1re  13548  1nprm  13789  163prm  14173  631prm  14175  strle2  14291  strle3  14292  2strstr  14295  rngstr  14306  srngfn  14314  lmodstr  14323  ipsstr  14330  phlstr  14340  topgrpstr  14348  otpsstr  14355  odrngstr  14366  imasvalstr  14411  ipostr  15344  0frgp  16297  cnfldstr  17842  zlmlem  17970  thlle  18144  tnglem  20248  iscmet3lem3  20823  mbfimaopnlem  21155  mbfsup  21164  mbfi1fseqlem6  21220  aalioulem3  21822  aaliou3lem3  21832  dvradcnv  21908  asin1  22311  log2cnv  22361  log2tlbnd  22362  mule1  22508  bposlem5  22649  bposlem8  22652  trkgstr  22927  0pth  23491  ex-fl  23676  blocnilem  24226  norm3difi  24571  norm3adifii  24572  bcsiALT  24603  nmopsetn0  25291  nmfnsetn0  25304  nmopge0  25337  nmfnge0  25353  0bdop  25419  nmcexi  25452  opsqrlem6  25571  dya2iocct  26717  signswbase  26977  signswplusg  26978  signswch  26984  subfaclim  27098  faclim  27574  cntotbnd  28721  diophren  29178  algstr  29560  stirlinglem1  29895  exple2lt6  30797  taupilem2  35712