Theorem snsstp1 4709

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 4707	. . 3 ⊢ {𝐴} ⊆ {𝐴, 𝐵}
2		ssun1 4099	. . 3 ⊢ {𝐴, 𝐵} ⊆ ({𝐴, 𝐵} ∪ {𝐶})
3	1, 2	sstri 3924	. 2 ⊢ {𝐴} ⊆ ({𝐴, 𝐵} ∪ {𝐶})
4		df-tp 4530	. 2 ⊢ {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶})
5	3, 4	sseqtrri 3952	1 ⊢ {𝐴} ⊆ {𝐴, 𝐵, 𝐶}

Syntax hints:   ∪ cun 3879   ⊆ wss 3881  {csn 4525  {cpr 4527  {ctp 4529

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-un 3886  df-in 3888  df-ss 3898  df-pr 4528  df-tp 4530

This theorem is referenced by:  fr3nr  7474  rngbase  16612  srngbase  16620  lmodbase  16629  ipsbase  16636  ipssca  16639  phlbase  16646  topgrpbas  16654  otpsbas  16661  odrngbas  16672  odrngtset  16675  prdssca  16721  prdsbas  16722  prdstset  16731  imasbas  16777  imassca  16784  imastset  16787  fucbas  17222  setcbas  17330  catcbas  17349  estrcbas  17367  cnfldbas  20095  cnfldtset  20099  psrbas  20616  psrsca  20627  trkgbas  26239  idlsrgbas  31057  signswch  31941  algbase  40122  clsk1indlem4  40747  clsk1indlem1  40748  rngcbasALTV  44607  ringcbasALTV  44670