Theorem snsstp1 4841

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 4839	. . 3 ⊢ {𝐴} ⊆ {𝐴, 𝐵}
2		ssun1 4201	. . 3 ⊢ {𝐴, 𝐵} ⊆ ({𝐴, 𝐵} ∪ {𝐶})
3	1, 2	sstri 4018	. 2 ⊢ {𝐴} ⊆ ({𝐴, 𝐵} ∪ {𝐶})
4		df-tp 4653	. 2 ⊢ {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶})
5	3, 4	sseqtrri 4046	1 ⊢ {𝐴} ⊆ {𝐴, 𝐵, 𝐶}

Syntax hints:   ∪ cun 3974   ⊆ wss 3976  {csn 4648  {cpr 4650  {ctp 4652

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-un 3981  df-ss 3993  df-pr 4651  df-tp 4653

This theorem is referenced by:  fr3nr  7807  rngbase  17358  srngbase  17369  lmodbase  17385  ipsbase  17396  ipssca  17399  phlbase  17406  topgrpbas  17421  otpsbas  17436  odrngbas  17463  odrngtset  17466  prdssca  17516  prdsbas  17517  prdstset  17526  imasbas  17572  imassca  17579  imastset  17582  fucbas  18029  setcbas  18145  catcbas  18168  estrcbas  18193  cnfldbas  21391  cnfldtset  21397  cnfldbasOLD  21406  cnfldtsetOLD  21410  psrbas  21976  psrsca  21990  trkgbas  28471  rlocbas  33239  rlocaddval  33240  rlocmulval  33241  idlsrgbas  33497  signswch  34538  algbase  43135  clsk1indlem4  44006  clsk1indlem1  44007  rngcbasALTV  47989  ringcbasALTV  48023  mndtcbasval  48753