Theorem eqimss2i 4041

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

Syntax hints:   = wceq 1534   ⊆ wss 3947

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-9 2109  ax-ext 2697

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1775  df-cleq 2718  df-ss 3964

This theorem is referenced by:  cotr3  14983  supcvg  15860  prodfclim1  15897  ef0lem  16080  1strbas  17230  1strbasOLD  17231  restid  17448  cayley  19412  gsumval3  19905  gsumzaddlem  19919  kgencn3  23553  hmeores  23766  opnfbas  23837  tsmsf1o  24140  ust0  24215  icchmeo  24956  icchmeoOLD  24957  plyeq0lem  26237  ulmdvlem1  26429  basellem7  27115  basellem9  27117  dchrisumlem3  27520  structvtxvallem  28956  struct2griedg  28964  gsumhashmul  32925  cycpmfvlem  32990  cycpmfv3  32993  constr01  33600  ivthALT  36047  aomclem4  42718  hashnzfzclim  43996  binomcxplemrat  44024  climsuselem1  45228  gsumfsupp  47559