Theorem eqimss2i 3984

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

Syntax hints:   = wceq 1541   ⊆ wss 3891

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1544  df-ex 1786  df-sb 2071  df-clab 2717  df-cleq 2731  df-clel 2817  df-v 3432  df-in 3898  df-ss 3908

This theorem is referenced by:  cotr3  14670  supcvg  15549  prodfclim1  15586  ef0lem  15769  1strbas  16910  1strbasOLD  16911  restid  17125  cayley  19003  gsumval3  19489  gsumzaddlem  19503  kgencn3  22690  hmeores  22903  opnfbas  22974  tsmsf1o  23277  ust0  23352  icchmeo  24085  plyeq0lem  25352  ulmdvlem1  25540  basellem7  26217  basellem9  26219  dchrisumlem3  26620  structvtxvallem  27371  struct2griedg  27379  gsumhashmul  31295  cycpmfvlem  31358  cycpmfv3  31361  ivthALT  34503  aomclem4  40862  hashnzfzclim  41893  binomcxplemrat  41921  climsuselem1  43102  gsumfsupp  45328