Theorem eqbrtri 4471

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

Hypotheses

Ref	Expression
eqbrtr.1
eqbrtr.2

Assertion

Ref	Expression
eqbrtri

Proof of Theorem eqbrtri

Step	Hyp	Ref	Expression
1		eqbrtr.2	. 2
2		eqbrtr.1	. . 3
3	2	breq1i 4459	. 2
4	1, 3	mpbir 209	1

Syntax hints:  =wceq 1395   class class class wbr 4452

This theorem is referenced by:  eqbrtrri  4473  3brtr4i  4480  infxpenc2  8420  infxpenc2OLD  8424  pm110.643  8578  pwsdompw  8605  r1om  8645  aleph1  8967  canthp1lem1  9051  pwxpndom2  9064  neg1lt0  10667  halflt1  10782  numlti  11028  sqlecan  12274  discr  12303  faclbnd3  12370  hashunlei  12483  hashge2el2dif  12521  geo2lim  13684  0.999...  13690  geoihalfsum  13691  cos2bnd  13923  sin4lt0  13930  eirrlem  13937  rpnnen2lem3  13950  rpnnen2lem9  13956  aleph1re  13978  1nprm  14222  163prm  14610  631prm  14612  strle2  14729  strle3  14730  2strstr  14733  rngstr  14744  srngfn  14752  lmodstr  14761  ipsstr  14768  phlstr  14778  topgrpstr  14786  otpsstr  14793  odrngstr  14804  imasvalstr  14849  ipostr  15783  0frgp  16797  cnfldstr  18422  zlmlem  18554  thlle  18728  tnglem  21154  iscmet3lem3  21729  mbfimaopnlem  22062  mbfsup  22071  mbfi1fseqlem6  22127  aalioulem3  22730  aaliou3lem3  22740  dvradcnv  22816  asin1  23225  log2cnv  23275  log2tlbnd  23276  mule1  23422  bposlem5  23563  bposlem8  23566  trkgstr  23840  0pth  24572  ex-fl  25168  blocnilem  25719  norm3difi  26064  norm3adifii  26065  bcsiALT  26096  nmopsetn0  26784  nmfnsetn0  26797  nmopge0  26830  nmfnge0  26846  0bdop  26912  nmcexi  26945  opsqrlem6  27064  locfinref  27844  dya2iocct  28251  signswch  28518  subfaclim  28632  logi  29121  faclim  29171  cntotbnd  30292  diophren  30747  algstr  31126  binomcxplemnn0  31254  binomcxplemrat  31255  stirlinglem1  31856  dirkercncflem1  31885  fouriersw  32014  1strstr  32560  exple2lt6  32957  taupilem2  37697

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  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 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-rab 2816  df-v 3111  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-sn 4030  df-pr 4032  df-op 4036  df-br 4453