Theorem eqimss2i 4008

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

Syntax hints:   = wceq 1540   ⊆ wss 3914

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-ss 3931

This theorem is referenced by:  cotr3  14944  supcvg  15822  prodfclim1  15859  ef0lem  16044  1strbas  17194  restid  17396  cayley  19344  gsumval3  19837  gsumzaddlem  19851  kgencn3  23445  hmeores  23658  opnfbas  23729  tsmsf1o  24032  ust0  24107  icchmeo  24838  icchmeoOLD  24839  plyeq0lem  26115  ulmdvlem1  26309  basellem7  26997  basellem9  26999  dchrisumlem3  27402  structvtxvallem  28947  struct2griedg  28955  gsumhashmul  33001  cycpmfvlem  33069  cycpmfv3  33072  constr01  33732  ivthALT  36323  aomclem4  43046  hashnzfzclim  44311  binomcxplemrat  44339  climsuselem1  45605  gsumfsupp  48170