Theorem eqimss2i 3983

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

Syntax hints:   = wceq 1542   ⊆ wss 3889

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 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2728  df-ss 3906

This theorem is referenced by:  cotr3  14940  supcvg  15821  prodfclim1  15858  ef0lem  16043  1strbas  17194  restid  17396  cayley  19389  gsumval3  19882  gsumzaddlem  19896  kgencn3  23523  hmeores  23736  opnfbas  23807  tsmsf1o  24110  ust0  24185  icchmeo  24908  plyeq0lem  26175  ulmdvlem1  26365  basellem7  27050  basellem9  27052  dchrisumlem3  27454  structvtxvallem  29089  struct2griedg  29097  gsumhashmul  33128  cycpmfvlem  33173  cycpmfv3  33176  constr01  33886  ivthALT  36517  aomclem4  43485  hashnzfzclim  44749  binomcxplemrat  44777  climsuselem1  46037  gsumfsupp  48658