Theorem snsstp1 4772

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 4770	. . 3 ⊢ {𝐴} ⊆ {𝐴, 𝐵}
2		ssun1 4130	. . 3 ⊢ {𝐴, 𝐵} ⊆ ({𝐴, 𝐵} ∪ {𝐶})
3	1, 2	sstri 3943	. 2 ⊢ {𝐴} ⊆ ({𝐴, 𝐵} ∪ {𝐶})
4		df-tp 4585	. 2 ⊢ {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶})
5	3, 4	sseqtrri 3983	1 ⊢ {𝐴} ⊆ {𝐴, 𝐵, 𝐶}

Syntax hints:   ∪ cun 3899   ⊆ wss 3901  {csn 4580  {cpr 4582  {ctp 4584

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-un 3906  df-ss 3918  df-pr 4583  df-tp 4585

This theorem is referenced by:  fr3nr  7717  rngbase  17219  srngbase  17230  lmodbase  17246  ipsbase  17257  ipssca  17260  phlbase  17267  topgrpbas  17282  otpsbas  17297  odrngbas  17324  odrngtset  17327  prdssca  17376  prdsbas  17377  prdstset  17386  imasbas  17433  imassca  17440  imastset  17443  fucbas  17887  setcbas  18002  catcbas  18025  estrcbas  18048  cnfldbas  21313  cnfldtset  21319  cnfldbasOLD  21328  cnfldtsetOLD  21332  psrbas  21889  psrsca  21903  trkgbas  28517  rlocbas  33349  rlocaddval  33350  rlocmulval  33351  idlsrgbas  33585  signswch  34718  algbase  43412  clsk1indlem4  44281  clsk1indlem1  44282  cycl3grtri  48189  rngcbasALTV  48508  ringcbasALTV  48542  catbas  49467  mndtcbasval  49821