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 1560   ⊆ wss 3904

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1800  df-cleq 2754  df-ss 3921

This theorem is referenced by:  cotr3  14991  supcvg  15886  prodfclim1  15923  ef0lem  16108  1strbas  17260  restid  17462  cayley  19454  gsumval3  19947  gsumzaddlem  19961  kgencn3  23615  hmeores  23828  opnfbas  23899  tsmsf1o  24202  ust0  24277  icchmeo  25000  plyeq0lem  26267  ulmdvlem1  26460  basellem7  27148  basellem9  27150  dchrisumlem3  27552  structvtxvallem  29218  struct2griedg  29226  gsumhashmul  33244  cycpmfvlem  33289  cycpmfv3  33292  constr01  34036  ivthALT  36692  aomclem4  43631  hashnzfzclim  44895  binomcxplemrat  44923  climsuselem1  46180  gsumfsupp  48801