Theorem eqimss2i 3976

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

Syntax hints:   = wceq 1539   ⊆ wss 3883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-in 3890  df-ss 3900

This theorem is referenced by:  cotr3  14617  supcvg  15496  prodfclim1  15533  ef0lem  15716  1strbas  16856  restid  17061  cayley  18937  gsumval3  19423  gsumzaddlem  19437  kgencn3  22617  hmeores  22830  opnfbas  22901  tsmsf1o  23204  ust0  23279  icchmeo  24010  plyeq0lem  25276  ulmdvlem1  25464  basellem7  26141  basellem9  26143  dchrisumlem3  26544  structvtxvallem  27293  struct2griedg  27301  gsumhashmul  31218  cycpmfvlem  31281  cycpmfv3  31284  ivthALT  34451  aomclem4  40798  hashnzfzclim  41829  binomcxplemrat  41857  climsuselem1  43038  gsumfsupp  45264