Theorem eqimss2i 3992

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

This proof depends on syntax axioms:   = wceq 1570   ⊆ wss 3899

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2732

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

This theorem is used by:  cotr3  15052  supcvg  15946  prodfclim1  15983  ef0lem  16165  1strbas  17317  restid  17519  cayley  19542  gsumval3  20035  gsumzaddlem  20049  kgencn3  23785  hmeores  23998  opnfbas  24069  tsmsf1o  24372  ust0  24447  icchmeo  25170  plyeq0lem  26437  ulmdvlem1  26637  basellem7  27324  basellem9  27326  dchrisumlem3  27728  structvtxvallem  29478  struct2griedg  29486  gsumhashmul  33508  cycpmfvlem  33553  cycpmfv3  33556  constr01  34253  ivthALT  36955  aomclem4  43899  hashnzfzclim  45147  binomcxplemrat  45175  climsuselem1  46438  gsumfsupp  49098