Theorem eqimss2i 4006

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

Syntax hints:   = wceq 1567   ⊆ wss 3913

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-cleq 2761  df-ss 3930

This theorem is referenced by:  cotr3  15014  supcvg  15909  prodfclim1  15946  ef0lem  16131  1strbas  17283  restid  17485  cayley  19483  gsumval3  19976  gsumzaddlem  19990  kgencn3  23683  hmeores  23896  opnfbas  23967  tsmsf1o  24270  ust0  24345  icchmeo  25068  plyeq0lem  26335  ulmdvlem1  26528  basellem7  27216  basellem9  27218  dchrisumlem3  27620  structvtxvallem  29310  struct2griedg  29318  gsumhashmul  33327  cycpmfvlem  33372  cycpmfv3  33375  constr01  34076  ivthALT  36734  aomclem4  43675  hashnzfzclim  44923  binomcxplemrat  44951  climsuselem1  46214  gsumfsupp  48835