Theorem eqimss2i 4005

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

Syntax hints:   = wceq 1540   ⊆ wss 3911

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 3928

This theorem is referenced by:  cotr3  14920  supcvg  15798  prodfclim1  15835  ef0lem  16020  1strbas  17170  restid  17372  cayley  19320  gsumval3  19813  gsumzaddlem  19827  kgencn3  23421  hmeores  23634  opnfbas  23705  tsmsf1o  24008  ust0  24083  icchmeo  24814  icchmeoOLD  24815  plyeq0lem  26091  ulmdvlem1  26285  basellem7  26973  basellem9  26975  dchrisumlem3  27378  structvtxvallem  28923  struct2griedg  28931  gsumhashmul  32974  cycpmfvlem  33042  cycpmfv3  33045  constr01  33705  ivthALT  36296  aomclem4  43019  hashnzfzclim  44284  binomcxplemrat  44312  climsuselem1  45578  gsumfsupp  48143