Theorem eqimss2i 3974

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 3952	1 ⊢ 𝐵 ⊆ 𝐴

Syntax hints:   = wceq 1538   ⊆ wss 3881

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-in 3888  df-ss 3898

This theorem is referenced by:  cotr3  14329  supcvg  15203  prodfclim1  15241  ef0lem  15424  1strbas  16591  restid  16699  cayley  18534  gsumval3  19020  gsumzaddlem  19034  kgencn3  22163  hmeores  22376  opnfbas  22447  tsmsf1o  22750  ust0  22825  icchmeo  23546  plyeq0lem  24807  ulmdvlem1  24995  basellem7  25672  basellem9  25674  dchrisumlem3  26075  structvtxvallem  26813  struct2griedg  26821  gsumhashmul  30741  cycpmfvlem  30804  cycpmfv3  30807  ivthALT  33796  aomclem4  40001  hashnzfzclim  41026  binomcxplemrat  41054  climsuselem1  42249  gsumfsupp  44442