Theorem eqimss2i 4042

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

Syntax hints:   = wceq 1541   ⊆ wss 3947

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476  df-in 3954  df-ss 3964

This theorem is referenced by:  cotr3  14921  supcvg  15798  prodfclim1  15835  ef0lem  16018  1strbas  17157  1strbasOLD  17158  restid  17375  cayley  19276  gsumval3  19769  gsumzaddlem  19783  kgencn3  23053  hmeores  23266  opnfbas  23337  tsmsf1o  23640  ust0  23715  icchmeo  24448  plyeq0lem  25715  ulmdvlem1  25903  basellem7  26580  basellem9  26582  dchrisumlem3  26983  structvtxvallem  28269  struct2griedg  28277  gsumhashmul  32195  cycpmfvlem  32258  cycpmfv3  32261  gg-icchmeo  35158  ivthALT  35208  aomclem4  41784  hashnzfzclim  43066  binomcxplemrat  43094  climsuselem1  44309  gsumfsupp  46578