Theorem eqbrtri 4445

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

Syntax hints:   = wceq 1437   class class class wbr 4426

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-rab 2791  df-v 3089  df-dif 3445  df-un 3447  df-in 3449  df-ss 3456  df-nul 3768  df-if 3916  df-sn 4003  df-pr 4005  df-op 4009  df-br 4427

This theorem is referenced by:  eqbrtrri  4447  3brtr4i  4454  infxpenc2  8451  pm110.643  8605  pwsdompw  8632  r1om  8672  aleph1  8994  canthp1lem1  9076  pwxpndom2  9089  neg1lt0  10716  halflt1  10831  numlti  11075  sqlecan  12378  discr  12406  faclbnd3  12474  hashunlei  12592  hashge2el2dif  12630  geo2lim  13909  0.999...  13915  geoihalfsum  13916  cos2bnd  14220  sin4lt0  14227  eirrlem  14234  rpnnen2lem3  14247  rpnnen2lem9  14253  aleph1re  14275  1nprm  14600  163prm  15059  631prm  15061  strle2  15184  strle3  15185  1strstr  15188  2strstr  15192  rngstr  15203  srngfn  15211  lmodstr  15220  ipsstr  15227  phlstr  15237  topgrpstr  15245  otpsstr  15252  odrngstr  15263  imasvalstr  15309  ipostr  16350  0frgp  17364  cnfldstr  18907  zlmlem  19019  thlle  19191  tnglem  21579  iscmet3lem3  22153  mbfimaopnlem  22488  mbfsup  22497  mbfi1fseqlem6  22555  aalioulem3  23155  aaliou3lem3  23165  dvradcnv  23241  asin1  23685  log2cnv  23735  log2tlbnd  23736  mule1  23938  bposlem5  24079  bposlem8  24082  trkgstr  24355  0pth  25145  ex-fl  25742  blocnilem  26290  norm3difi  26635  norm3adifii  26636  bcsiALT  26667  nmopsetn0  27353  nmfnsetn0  27366  nmopge0  27399  nmfnge0  27415  0bdop  27481  nmcexi  27514  opsqrlem6  27633  locfinref  28507  dya2iocct  28941  signswch  29238  subfaclim  29699  logi  30157  faclim  30169  taupilem2  31468  cntotbnd  31832  diophren  35365  algstr  35742  binomcxplemnn0  36335  binomcxplemrat  36336  stirlinglem1  37505  dirkercncflem1  37534  fouriersw  37663  meaiunlelem  37815  exple2lt6  38909  3halfnz  39078  nnlog2ge0lt1  39138