Theorem eqimss2i 3998

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

Syntax hints:   = wceq 1570   ⊆ wss 3905

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-cleq 2755  df-ss 3922

This theorem is referenced by:  cotr3  15011  supcvg  15906  prodfclim1  15943  ef0lem  16127  1strbas  17279  restid  17481  cayley  19479  gsumval3  19972  gsumzaddlem  19986  kgencn3  23715  hmeores  23928  opnfbas  23999  tsmsf1o  24302  ust0  24377  icchmeo  25100  plyeq0lem  26367  ulmdvlem1  26563  basellem7  27251  basellem9  27253  dchrisumlem3  27655  structvtxvallem  29370  struct2griedg  29378  gsumhashmul  33387  cycpmfvlem  33432  cycpmfv3  33435  constr01  34132  ivthALT  36846  aomclem4  43784  hashnzfzclim  45032  binomcxplemrat  45060  climsuselem1  46323  gsumfsupp  48947