Theorem snsstp1 4775

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 4773	. . 3 ⊢ {𝐴} ⊆ {𝐴, 𝐵}
2		ssun1 4179	. . 3 ⊢ {𝐴, 𝐵} ⊆ ({𝐴, 𝐵} ∪ {𝐶})
3	1, 2	sstri 3922	. 2 ⊢ {𝐴} ⊆ ({𝐴, 𝐵} ∪ {𝐶})
4		df-tp 4593	. 2 ⊢ {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶})
5	3, 4	sseqtrri 3962	1 ⊢ {𝐴} ⊆ {𝐴, 𝐵, 𝐶}

This proof depends on syntax axioms:   ⊆ wss 3900   ∪ cun 4152  {csn 4588  {cpr 4590  {ctp 4592

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-ss 3901  df-un 4154  df-pr 4591  df-tp 4593

This theorem is used by:  fr3nr  7807  rngbase  17496  srngbase  17507  lmodbase  17523  ipsbase  17534  ipssca  17537  phlbase  17544  topgrpbas  17559  otpsbas  17574  odrngbas  17601  odrngtset  17604  prdssca  17653  prdsbas  17654  prdstset  17663  imasbas  17710  imassca  17717  imastset  17720  fucbas  18164  setcbas  18279  catcbas  18302  estrcbas  18325  cnfldbas  21709  cnfldtset  21715  psrbas  22269  psrsca  22282  trkgbas  28934  angmgmlem  29422  angmgmbas  29425  rlocbas  33896  rlocaddval  33897  rlocmulval  33898  idlsrgbas  34103  signswch  35257  algbase  44366  clsk1indlem4  45234  clsk1indlem1  45235  cycl3grtri  49248  rngcbasALTV  49566  ringcbasALTV  49600  catbas  50551  mndtcbasval  50921