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  19328  gsumval3  19821  gsumzaddlem  19835  kgencn3  23478  hmeores  23691  opnfbas  23762  tsmsf1o  24065  ust0  24140  icchmeo  24871  icchmeoOLD  24872  plyeq0lem  26148  ulmdvlem1  26342  basellem7  27030  basellem9  27032  dchrisumlem3  27435  structvtxvallem  29000  struct2griedg  29008  gsumhashmul  33044  cycpmfvlem  33084  cycpmfv3  33087  constr01  33725  ivthALT  36316  aomclem4  43039  hashnzfzclim  44304  binomcxplemrat  44332  climsuselem1  45598  gsumfsupp  48163