Theorem eqimss2i 3558

Description: Infer subclass relationship from equality. (Contributed by NM, 7-Jan-2007.)

Hypothesis

Ref	Expression
eqimssi.1

Assertion

Ref	Expression
eqimss2i

Proof of Theorem eqimss2i

Step	Hyp	Ref	Expression
1		ssid 3522	. 2
2		eqimssi.1	. 2
3	1, 2	sseqtr4i 3536	1

Syntax hints:  =wceq 1395  C_wss 3475

This theorem is referenced by:  supcvg  13667  prodfclim1  13702  ef0lem  13814  restid  14831  cayley  16439  gsumval3OLD  16908  gsumval3  16911  gsumzaddlem  16934  gsumzaddlemOLD  16936  kgencn3  20059  hmeores  20272  opnfbas  20343  tsmsf1o  20647  ust0  20722  icchmeo  21441  plyeq0lem  22607  ulmdvlem1  22795  basellem7  23360  basellem9  23362  dchrisumlem3  23676  ivthALT  30153  aomclem4  31003  hashnzfzclim  31227  binomcxplemrat  31255  climsuselem1  31613  1strbas  32561  cotr3  37788

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