Theorem eqimss2i 4057

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

Syntax hints:   = wceq 1537   ⊆ wss 3963

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1777  df-cleq 2727  df-ss 3980

This theorem is referenced by:  cotr3  15014  supcvg  15889  prodfclim1  15926  ef0lem  16111  1strbas  17262  1strbasOLD  17263  restid  17480  cayley  19447  gsumval3  19940  gsumzaddlem  19954  kgencn3  23582  hmeores  23795  opnfbas  23866  tsmsf1o  24169  ust0  24244  icchmeo  24985  icchmeoOLD  24986  plyeq0lem  26264  ulmdvlem1  26458  basellem7  27145  basellem9  27147  dchrisumlem3  27550  structvtxvallem  29052  struct2griedg  29060  gsumhashmul  33047  cycpmfvlem  33115  cycpmfv3  33118  constr01  33747  ivthALT  36318  aomclem4  43046  hashnzfzclim  44318  binomcxplemrat  44346  climsuselem1  45563  gsumfsupp  48026