Theorem eqimss2i 3980

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 3943	. 2 ⊢ 𝐵 ⊆ 𝐵
2		eqimssi.1	. 2 ⊢ 𝐴 = 𝐵
3	1, 2	sseqtrri 3958	1 ⊢ 𝐵 ⊆ 𝐴

Syntax hints:   = wceq 1539   ⊆ wss 3887

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3434  df-in 3894  df-ss 3904

This theorem is referenced by:  cotr3  14689  supcvg  15568  prodfclim1  15605  ef0lem  15788  1strbas  16929  1strbasOLD  16930  restid  17144  cayley  19022  gsumval3  19508  gsumzaddlem  19522  kgencn3  22709  hmeores  22922  opnfbas  22993  tsmsf1o  23296  ust0  23371  icchmeo  24104  plyeq0lem  25371  ulmdvlem1  25559  basellem7  26236  basellem9  26238  dchrisumlem3  26639  structvtxvallem  27390  struct2griedg  27398  gsumhashmul  31316  cycpmfvlem  31379  cycpmfv3  31382  ivthALT  34524  aomclem4  40882  hashnzfzclim  41940  binomcxplemrat  41968  climsuselem1  43148  gsumfsupp  45376