Theorem eqimss2i 3997

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

Syntax hints:   = wceq 1540   ⊆ wss 3903

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-ss 3920

This theorem is referenced by:  cotr3  14885  supcvg  15763  prodfclim1  15800  ef0lem  15985  1strbas  17135  restid  17337  cayley  19293  gsumval3  19786  gsumzaddlem  19800  kgencn3  23443  hmeores  23656  opnfbas  23727  tsmsf1o  24030  ust0  24105  icchmeo  24836  icchmeoOLD  24837  plyeq0lem  26113  ulmdvlem1  26307  basellem7  26995  basellem9  26997  dchrisumlem3  27400  structvtxvallem  28965  struct2griedg  28973  gsumhashmul  33014  cycpmfvlem  33054  cycpmfv3  33057  constr01  33709  ivthALT  36309  aomclem4  43030  hashnzfzclim  44295  binomcxplemrat  44323  climsuselem1  45588  gsumfsupp  48166