Theorem eqimss2i 3623

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

Syntax hints:   = wceq 1475   ⊆ wss 3540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-in 3547  df-ss 3554

This theorem is referenced by:  cotr3  13565  supcvg  14427  prodfclim1  14464  ef0lem  14648  1strbas  15806  restid  15917  cayley  17657  gsumval3  18131  gsumzaddlem  18144  kgencn3  21171  hmeores  21384  opnfbas  21456  tsmsf1o  21758  ust0  21833  icchmeo  22548  plyeq0lem  23770  ulmdvlem1  23958  basellem7  24613  basellem9  24615  dchrisumlem3  24980  ivthALT  31500  aomclem4  36645  hashnzfzclim  37543  binomcxplemrat  37571  climsuselem1  38674