Theorem eqbrtri 4466

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

Syntax hints:   = wceq 1379   class class class wbr 4447

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-rab 2823  df-v 3115  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-nul 3786  df-if 3940  df-sn 4028  df-pr 4030  df-op 4034  df-br 4448

This theorem is referenced by:  eqbrtrri  4468  3brtr4i  4475  infxpenc2  8400  infxpenc2OLD  8404  pm110.643  8558  pwsdompw  8585  r1om  8625  aleph1  8947  canthp1lem1  9031  pwxpndom2  9044  neg1lt0  10643  halflt1  10758  numlti  11001  sqlecan  12243  discr  12272  faclbnd3  12339  hashunlei  12449  hashge2el2dif  12488  geo2lim  13650  0.999...  13656  geoihalfsum  13657  cos2bnd  13787  sin4lt0  13794  eirrlem  13801  rpnnen2lem3  13814  rpnnen2lem9  13820  aleph1re  13842  1nprm  14084  163prm  14471  631prm  14473  strle2  14590  strle3  14591  2strstr  14594  rngstr  14605  srngfn  14613  lmodstr  14622  ipsstr  14629  phlstr  14639  topgrpstr  14647  otpsstr  14654  odrngstr  14665  imasvalstr  14710  ipostr  15643  0frgp  16612  cnfldstr  18233  zlmlem  18361  thlle  18535  tnglem  20981  iscmet3lem3  21556  mbfimaopnlem  21889  mbfsup  21898  mbfi1fseqlem6  21954  aalioulem3  22556  aaliou3lem3  22566  dvradcnv  22642  asin1  23050  log2cnv  23100  log2tlbnd  23101  mule1  23247  bposlem5  23388  bposlem8  23391  trkgstr  23665  0pth  24345  ex-fl  24942  blocnilem  25492  norm3difi  25837  norm3adifii  25838  bcsiALT  25869  nmopsetn0  26557  nmfnsetn0  26570  nmopge0  26603  nmfnge0  26619  0bdop  26685  nmcexi  26718  opsqrlem6  26837  dya2iocct  28002  signswbase  28262  signswplusg  28263  signswch  28269  subfaclim  28383  faclim  29024  cntotbnd  30122  diophren  30578  algstr  30958  stirlinglem1  31601  dirkercncflem1  31630  fouriersw  31759  exple2lt6  32253  taupilem2  36985