Theorem eqimss2i 3997

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

Syntax hints:   = wceq 1542   ⊆ wss 3903

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-ss 3920

This theorem is referenced by:  cotr3  14913  supcvg  15791  prodfclim1  15828  ef0lem  16013  1strbas  17163  restid  17365  cayley  19355  gsumval3  19848  gsumzaddlem  19862  kgencn3  23514  hmeores  23727  opnfbas  23798  tsmsf1o  24101  ust0  24176  icchmeo  24906  icchmeoOLD  24907  plyeq0lem  26183  ulmdvlem1  26377  basellem7  27065  basellem9  27067  dchrisumlem3  27470  structvtxvallem  29105  struct2griedg  29113  gsumhashmul  33161  cycpmfvlem  33206  cycpmfv3  33209  constr01  33920  ivthALT  36551  aomclem4  43414  hashnzfzclim  44678  binomcxplemrat  44706  climsuselem1  45967  gsumfsupp  48542