Theorem eqimss2i 3991

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

Syntax hints:   = wceq 1541   ⊆ wss 3897

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2723  df-ss 3914

This theorem is referenced by:  cotr3  14885  supcvg  15763  prodfclim1  15800  ef0lem  15985  1strbas  17135  restid  17337  cayley  19326  gsumval3  19819  gsumzaddlem  19833  kgencn3  23473  hmeores  23686  opnfbas  23757  tsmsf1o  24060  ust0  24135  icchmeo  24865  icchmeoOLD  24866  plyeq0lem  26142  ulmdvlem1  26336  basellem7  27024  basellem9  27026  dchrisumlem3  27429  structvtxvallem  28998  struct2griedg  29006  gsumhashmul  33041  cycpmfvlem  33081  cycpmfv3  33084  constr01  33755  ivthALT  36377  aomclem4  43098  hashnzfzclim  44363  binomcxplemrat  44391  climsuselem1  45655  gsumfsupp  48221