Theorem sseqtri 3535

Description: Substitution of equality into a subclass relationship. (Contributed by NM, 28-Jul-1995.)

Hypotheses

Ref	Expression
sseqtr.1
sseqtr.2

Assertion

Ref	Expression
sseqtri

Proof of Theorem sseqtri

Step	Hyp	Ref	Expression
1		sseqtr.1	. 2
2		sseqtr.2	. . 3
3	2	sseq2i 3528	. 2
4	1, 3	mpbi 208	1

Syntax hints:  =wceq 1395  C_wss 3475

This theorem is referenced by:  sseqtr4i  3536  eqimssi  3557  abssi  3574  ssun2  3667  unixpss  5123  0ima  5358  fvssunirn  5894  difex2  6607  oelim2  7263  omopthlem2  7324  sbthlem7  7653  unifpw  7843  fiuni  7908  rankuni  8302  rankc2  8310  rankxpu  8315  rankmapu  8317  rankxplim  8318  infxpenlem  8412  cf0  8652  fin23lem17  8739  fin23lem31  8744  smobeth  8982  nqerf  9329  dmrecnq  9367  ackbijnn  13640  divalglem2  14053  divalglem5  14055  bitsfzolem  14084  0bits  14089  bezoutlem2  14177  bezoutlem3  14178  odzcllem  14319  odzdvds  14322  unbenlem  14426  4sqlem13  14475  4sqlem14  14476  4sqlem17  14479  4sqlem18  14480  vdwlem8  14506  vdwnnlem3  14515  ramcl2lem  14527  ramtcl  14528  ramtub  14530  strle1  14728  prdsval  14852  xpsc0  14957  xpsc1  14958  wunfunc  15268  wunnat  15325  psssdm2  15845  tsrss  15853  gicer  16324  symgsssg  16492  symgfisg  16493  odlem2  16563  gexlem2  16602  torsubg  16860  gsumzaddlemOLD  16936  dprd2da  17091  zringlpirlem2  18510  zringlpirlem3  18511  zlpirlem2  18515  zlpirlem3  18516  pjfval  18737  pjpm  18739  eltg4i  19461  ntrss2  19558  isopn3  19567  mretopd  19593  leordtval2  19713  ptbasfi  20082  hmphtop  20279  hmpher  20285  restutop  20740  ucnprima  20785  tngtopn  21164  tgioo  21301  xrtgioo  21311  ovolicc2lem4  21931  nulmbl2  21947  iundisj  21958  dyadmax  22007  i1f1  22097  dvfval  22301  dvcnp2  22323  lhop1lem  22414  lhop2  22416  elqaalem1  22715  elqaalem3  22717  taylthlem2  22769  pserulm  22817  psercn2  22818  psercnlem2  22819  psercnlem1  22820  psercn  22821  pserdvlem1  22822  pserdvlem2  22823  pserdv  22824  pserdv2  22825  abelth  22836  dvlog  23032  efopnlem2  23038  logtayl  23041  cxpcn3lem  23121  cxpcn3  23122  resqrtcn  23123  dvatan  23266  atancn  23267  rlimcnp  23295  rlimcnp2  23296  wilthlem3  23344  ftalem4  23349  ftalem5  23350  dchrisum0lem2a  23702  cchhllem  24190  axlowdimlem6  24250  choc1  26245  chub2i  26388  span0  26460  spanuni  26462  sshhococi  26464  chsup0  26466  spansnpji  26496  mayetes3i  26648  nlelshi  26979  pjimai  27095  pj3i  27127  shatomistici  27280  hatomistici  27281  atcvat4i  27316  iundisjf  27448  idssxp  27469  rinvf1o  27472  mptctf  27544  iundisjfi  27601  xrge0mulgnn0  27677  xrge0iifcnv  27915  xrge0iifiso  27917  xrge0iifhom  27919  coinfliprv  28421  signsply0  28508  signstcl  28522  signstf  28523  kur14lem6  28655  mthmsta  28938  nocvxminlem  29450  nocvxmin  29451  nobndlem1  29452  nobndlem2  29453  onint1  29914  oninhaus  29915  dvtan  30065  itg2addnclem2  30067  ftc1anclem6  30095  filnetlem3  30198  filnetlem4  30199  heiborlem3  30309  isdrngo2  30361  elrfi  30626  mapfzcons1  30649  eldioph4b  30745  dnnumch3lem  30992  dnnumch3  30993  dgraalem  31094  dgraaub  31097  lcmcllem  31202  lcmledvds  31205  binomcxplemdvbinom  31258  binomcxplemdvsum  31260  binomcxplemnotnn0  31261  rabexgf  31399  fzssnn0  31522  sumnnodd  31636  lptioo2cn  31651  lptioo1cn  31652  fourierdlem31  31920  fourierdlem102  31991  fourierdlem114  32003  fouriercn  32015  elaa2lem  32016  etransclem48  32065  relopabVD  33701  bj-nuliotaALT  34587

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-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-in 3482  df-ss 3489