Theorem snsstp1 4776

Description: A singleton is a subset of an unordered triple containing its member. (Contributed by NM, 9-Oct-2013.)

Assertion

Ref	Expression
snsstp1	⊢ {𝐴} ⊆ {𝐴, 𝐵, 𝐶}

Proof of Theorem snsstp1

Step	Hyp	Ref	Expression
1		snsspr1 4774	. . 3 ⊢ {𝐴} ⊆ {𝐴, 𝐵}
2		ssun1 4132	. . 3 ⊢ {𝐴, 𝐵} ⊆ ({𝐴, 𝐵} ∪ {𝐶})
3	1, 2	sstri 3947	. 2 ⊢ {𝐴} ⊆ ({𝐴, 𝐵} ∪ {𝐶})
4		df-tp 4589	. 2 ⊢ {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶})
5	3, 4	sseqtrri 3987	1 ⊢ {𝐴} ⊆ {𝐴, 𝐵, 𝐶}

Syntax hints:   ∪ cun 3904   ⊆ wss 3906  {csn 4584  {cpr 4586  {ctp 4588

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-ext 2736

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-tru 1565  df-ex 1802  df-sb 2093  df-clab 2743  df-cleq 2756  df-clel 2839  df-v 3458  df-un 3911  df-ss 3923  df-pr 4587  df-tp 4589

This theorem is referenced by:  fr3nr  7757  rngbase  17330  srngbase  17341  lmodbase  17357  ipsbase  17368  ipssca  17371  phlbase  17378  topgrpbas  17393  otpsbas  17408  odrngbas  17435  odrngtset  17438  prdssca  17487  prdsbas  17488  prdstset  17497  imasbas  17544  imassca  17551  imastset  17554  fucbas  17998  setcbas  18113  catcbas  18136  estrcbas  18159  cnfldbas  21430  cnfldtset  21436  psrbas  21988  psrsca  22001  trkgbas  28616  rlocbas  33451  rlocaddval  33452  rlocmulval  33453  idlsrgbas  33702  signswch  34857  algbase  43756  clsk1indlem4  44625  clsk1indlem1  44626  cycl3grtri  48574  rngcbasALTV  48893  ringcbasALTV  48927  catbas  49852  mndtcbasval  50206