Theorem eqimss2i 3970

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

This proof depends on syntax axioms:   = wceq 1569   ⊆ wss 3896

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2752  df-ss 3897

This theorem is used by:  cotr3  15140  supcvg  16034  prodfclim1  16071  ef0lem  16253  1strbas  17411  restid  17613  cayley  19637  gsumval3  20130  gsumzaddlem  20144  kgencn3  23886  hmeores  24099  opnfbas  24170  tsmsf1o  24473  ust0  24548  icchmeo  25271  plyeq0lem  26538  ulmdvlem1  26736  basellem7  27423  basellem9  27425  dchrisumlem3  27827  structvtxvallem  29607  struct2griedg  29615  gsumhashmul  33678  cycpmfvlem  33723  cycpmfv3  33726  constr01  34424  ivthALT  37247  aomclem4  44196  hashnzfzclim  45443  binomcxplemrat  45471  climsuselem1  46755  gsumfsupp  49415