Theorem eqimss2i 3993

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

Syntax hints:   = wceq 1541   ⊆ wss 3899

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2726  df-ss 3916

This theorem is referenced by:  cotr3  14899  supcvg  15777  prodfclim1  15814  ef0lem  15999  1strbas  17149  restid  17351  cayley  19341  gsumval3  19834  gsumzaddlem  19848  kgencn3  23500  hmeores  23713  opnfbas  23784  tsmsf1o  24087  ust0  24162  icchmeo  24892  icchmeoOLD  24893  plyeq0lem  26169  ulmdvlem1  26363  basellem7  27051  basellem9  27053  dchrisumlem3  27456  structvtxvallem  29042  struct2griedg  29050  gsumhashmul  33099  cycpmfvlem  33143  cycpmfv3  33146  constr01  33848  ivthALT  36478  aomclem4  43241  hashnzfzclim  44505  binomcxplemrat  44533  climsuselem1  45795  gsumfsupp  48370