Theorem eqimss2i 3974

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

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

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 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-ext 2735

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

This theorem is used by:  cotr3  15174  supcvg  16069  prodfclim1  16106  ef0lem  16288  1strbas  17446  restid  17654  cayley  19679  gsumval3  20172  gsumzaddlem  20186  kgencn3  23932  hmeores  24145  opnfbas  24216  tsmsf1o  24519  ust0  24594  icchmeo  25317  plyeq0lem  26584  ulmdvlem1  26784  basellem7  27471  basellem9  27473  dchrisumlem3  27875  structvtxvallem  29655  struct2griedg  29663  gsumhashmul  33727  cycpmfvlem  33772  cycpmfv3  33775  constr01  34485  ivthALT  37338  aomclem4  44325  hashnzfzclim  45567  binomcxplemrat  45595  climsuselem1  46892  gsumfsupp  49552