Theorem eqbrtri 4475

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

Syntax hints:   = wceq 1395   class class class wbr 4456

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1614  df-nf 1618  df-sb 1741  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-rab 2816  df-v 3111  df-dif 3474  df-un 3476  df-in 3478  df-ss 3485  df-nul 3794  df-if 3945  df-sn 4033  df-pr 4035  df-op 4039  df-br 4457

This theorem is referenced by:  eqbrtrri  4477  3brtr4i  4484  infxpenc2  8416  infxpenc2OLD  8420  pm110.643  8574  pwsdompw  8601  r1om  8641  aleph1  8963  canthp1lem1  9047  pwxpndom2  9060  neg1lt0  10663  halflt1  10778  numlti  11024  sqlecan  12276  discr  12305  faclbnd3  12372  hashunlei  12486  hashge2el2dif  12524  geo2lim  13695  0.999...  13701  geoihalfsum  13702  cos2bnd  13934  sin4lt0  13941  eirrlem  13948  rpnnen2lem3  13961  rpnnen2lem9  13967  aleph1re  13989  1nprm  14233  163prm  14621  631prm  14623  strle2  14743  strle3  14744  1strstr  14747  2strstr  14751  rngstr  14762  srngfn  14770  lmodstr  14779  ipsstr  14786  phlstr  14796  topgrpstr  14804  otpsstr  14811  odrngstr  14822  imasvalstr  14868  ipostr  15909  0frgp  16923  cnfldstr  18548  zlmlem  18680  thlle  18854  tnglem  21279  iscmet3lem3  21854  mbfimaopnlem  22187  mbfsup  22196  mbfi1fseqlem6  22252  aalioulem3  22855  aaliou3lem3  22865  dvradcnv  22941  asin1  23350  log2cnv  23400  log2tlbnd  23401  mule1  23547  bposlem5  23688  bposlem8  23691  trkgstr  23965  0pth  24698  ex-fl  25294  blocnilem  25845  norm3difi  26190  norm3adifii  26191  bcsiALT  26222  nmopsetn0  26910  nmfnsetn0  26923  nmopge0  26956  nmfnge0  26972  0bdop  27038  nmcexi  27071  opsqrlem6  27190  locfinref  27997  dya2iocct  28412  signswch  28693  subfaclim  28807  logi  29296  faclim  29346  cntotbnd  30454  diophren  30909  algstr  31288  binomcxplemnn0  31416  binomcxplemrat  31417  stirlinglem1  32017  dirkercncflem1  32046  fouriersw  32175  exple2lt6  33059  taupilem2  37798