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 2733

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

This theorem is used by:  cotr3  15131  supcvg  16025  prodfclim1  16062  ef0lem  16244  1strbas  17402  restid  17604  cayley  19628  gsumval3  20121  gsumzaddlem  20135  kgencn3  23877  hmeores  24090  opnfbas  24161  tsmsf1o  24464  ust0  24539  icchmeo  25262  plyeq0lem  26529  ulmdvlem1  26727  basellem7  27414  basellem9  27416  dchrisumlem3  27818  structvtxvallem  29598  struct2griedg  29606  gsumhashmul  33628  cycpmfvlem  33673  cycpmfv3  33676  constr01  34374  ivthALT  37123  aomclem4  44058  hashnzfzclim  45305  binomcxplemrat  45333  climsuselem1  46618  gsumfsupp  49278