Theorem snsstp1 4752

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 4750	. . 3 ⊢ {𝐴} ⊆ {𝐴, 𝐵}
2		ssun1 4151	. . 3 ⊢ {𝐴, 𝐵} ⊆ ({𝐴, 𝐵} ∪ {𝐶})
3	1, 2	sstri 3979	. 2 ⊢ {𝐴} ⊆ ({𝐴, 𝐵} ∪ {𝐶})
4		df-tp 4575	. 2 ⊢ {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶})
5	3, 4	sseqtrri 4007	1 ⊢ {𝐴} ⊆ {𝐴, 𝐵, 𝐶}

Syntax hints:   ∪ cun 3937   ⊆ wss 3939  {csn 4570  {cpr 4572  {ctp 4574

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2160  ax-12 2176  ax-ext 2796

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1539  df-ex 1780  df-nf 1784  df-sb 2069  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2966  df-v 3499  df-un 3944  df-in 3946  df-ss 3955  df-pr 4573  df-tp 4575

This theorem is referenced by:  fr3nr  7497  rngbase  16623  srngbase  16631  lmodbase  16640  ipsbase  16647  ipssca  16650  phlbase  16657  topgrpbas  16665  otpsbas  16672  odrngbas  16683  odrngtset  16686  prdssca  16732  prdsbas  16733  prdstset  16742  imasbas  16788  imassca  16795  imastset  16798  fucbas  17233  setcbas  17341  catcbas  17360  estrcbas  17378  psrbas  20161  psrsca  20172  cnfldbas  20552  cnfldtset  20556  trkgbas  26234  signswch  31835  algbase  39784  clsk1indlem4  40400  clsk1indlem1  40401  rngcbasALTV  44261  ringcbasALTV  44324