Theorem eqimss2i 4029

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

Syntax hints:   = wceq 1536   ⊆ wss 3939

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 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2160  ax-12 2176  ax-ext 2796

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1539  df-ex 1780  df-nf 1784  df-sb 2069  df-clab 2803  df-cleq 2817  df-clel 2896  df-in 3946  df-ss 3955

This theorem is referenced by:  cotr3  14341  supcvg  15214  prodfclim1  15252  ef0lem  15435  1strbas  16602  restid  16710  cayley  18545  gsumval3  19030  gsumzaddlem  19044  kgencn3  22169  hmeores  22382  opnfbas  22453  tsmsf1o  22756  ust0  22831  icchmeo  23548  plyeq0lem  24803  ulmdvlem1  24991  basellem7  25667  basellem9  25669  dchrisumlem3  26070  structvtxvallem  26808  struct2griedg  26816  cycpmfvlem  30758  cycpmfv3  30761  ivthALT  33687  aomclem4  39663  hashnzfzclim  40660  binomcxplemrat  40688  climsuselem1  41894  gsumfsupp  44096