Theorem snsstp1 4818

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

Syntax hints:   ∪ cun 3945   ⊆ wss 3947  {csn 4627  {cpr 4629  {ctp 4631

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-tru 1542  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-v 3474  df-un 3952  df-in 3954  df-ss 3964  df-pr 4630  df-tp 4632

This theorem is referenced by:  fr3nr  7761  rngbase  17248  srngbase  17259  lmodbase  17275  ipsbase  17286  ipssca  17289  phlbase  17296  topgrpbas  17311  otpsbas  17326  odrngbas  17353  odrngtset  17356  prdssca  17406  prdsbas  17407  prdstset  17416  imasbas  17462  imassca  17469  imastset  17472  fucbas  17916  setcbas  18032  catcbas  18055  estrcbas  18080  cnfldbas  21148  cnfldtset  21152  psrbas  21716  psrsca  21727  trkgbas  27963  idlsrgbas  32892  signswch  33870  gg-cnfldbas  35475  gg-cnfldtset  35479  algbase  42222  clsk1indlem4  43097  clsk1indlem1  43098  rngcbasALTV  46969  ringcbasALTV  47032  mndtcbasval  47793