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

Syntax hints:   = wceq 1547   ⊆ wss 3883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2731  df-ss 3900

This theorem is referenced by:  cotr3  14931  supcvg  15812  prodfclim1  15849  ef0lem  16034  1strbas  17185  restid  17387  cayley  19380  gsumval3  19873  gsumzaddlem  19887  kgencn3  23541  hmeores  23754  opnfbas  23825  tsmsf1o  24128  ust0  24203  icchmeo  24926  plyeq0lem  26193  ulmdvlem1  26383  basellem7  27068  basellem9  27070  dchrisumlem3  27472  structvtxvallem  29107  struct2griedg  29115  gsumhashmul  33148  cycpmfvlem  33193  cycpmfv3  33196  constr01  33926  ivthALT  36563  aomclem4  43502  hashnzfzclim  44766  binomcxplemrat  44794  climsuselem1  46052  gsumfsupp  48673