Theorem eqimss2i 3693

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 3657	. 2 ⊢ 𝐵 ⊆ 𝐵
2		eqimssi.1	. 2 ⊢ 𝐴 = 𝐵
3	1, 2	sseqtr4i 3671	1 ⊢ 𝐵 ⊆ 𝐴

Syntax hints:   = wceq 1523   ⊆ wss 3607

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-in 3614  df-ss 3621

This theorem is referenced by:  cotr3  13763  supcvg  14632  prodfclim1  14669  ef0lem  14853  1strbas  16027  restid  16141  cayley  17880  gsumval3  18354  gsumzaddlem  18367  kgencn3  21409  hmeores  21622  opnfbas  21693  tsmsf1o  21995  ust0  22070  icchmeo  22787  plyeq0lem  24011  ulmdvlem1  24199  basellem7  24858  basellem9  24860  dchrisumlem3  25225  structvtxvallem  25954  struct2griedg  25965  ivthALT  32455  aomclem4  37944  hashnzfzclim  38838  binomcxplemrat  38866  climsuselem1  40157