Theorem eqimss2i 3999

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

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

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 2156  ax-ext 2737

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

This theorem is used by:  cotr3  15041  supcvg  15935  prodfclim1  15972  ef0lem  16156  1strbas  17308  restid  17510  cayley  19530  gsumval3  20023  gsumzaddlem  20037  kgencn3  23768  hmeores  23981  opnfbas  24052  tsmsf1o  24355  ust0  24430  icchmeo  25153  plyeq0lem  26420  ulmdvlem1  26616  basellem7  27304  basellem9  27306  dchrisumlem3  27708  structvtxvallem  29427  struct2griedg  29435  gsumhashmul  33453  cycpmfvlem  33498  cycpmfv3  33501  constr01  34198  ivthALT  36905  aomclem4  43844  hashnzfzclim  45092  binomcxplemrat  45120  climsuselem1  46383  gsumfsupp  49006