Theorem eqimss2i 3995

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

Syntax hints:   = wceq 1541   ⊆ wss 3901

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 2708

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

This theorem is referenced by:  cotr3  14901  supcvg  15779  prodfclim1  15816  ef0lem  16001  1strbas  17151  restid  17353  cayley  19343  gsumval3  19836  gsumzaddlem  19850  kgencn3  23502  hmeores  23715  opnfbas  23786  tsmsf1o  24089  ust0  24164  icchmeo  24894  icchmeoOLD  24895  plyeq0lem  26171  ulmdvlem1  26365  basellem7  27053  basellem9  27055  dchrisumlem3  27458  structvtxvallem  29093  struct2griedg  29101  gsumhashmul  33150  cycpmfvlem  33194  cycpmfv3  33197  constr01  33899  ivthALT  36529  aomclem4  43299  hashnzfzclim  44563  binomcxplemrat  44591  climsuselem1  45853  gsumfsupp  48428