Theorem snsstp1 4787

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 4785	. . 3 ⊢ {𝐴} ⊆ {𝐴, 𝐵}
2		ssun1 4139	. . 3 ⊢ {𝐴, 𝐵} ⊆ ({𝐴, 𝐵} ∪ {𝐶})
3	1, 2	sstri 3954	. 2 ⊢ {𝐴} ⊆ ({𝐴, 𝐵} ∪ {𝐶})
4		df-tp 4599	. 2 ⊢ {𝐴, 𝐵, 𝐶} = ({𝐴, 𝐵} ∪ {𝐶})
5	3, 4	sseqtrri 3994	1 ⊢ {𝐴} ⊆ {𝐴, 𝐵, 𝐶}

Syntax hints:   ∪ cun 3911   ⊆ wss 3913  {csn 4594  {cpr 4596  {ctp 4598

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-8 2152  ax-9 2160  ax-ext 2742

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1571  df-ex 1808  df-sb 2099  df-clab 2749  df-cleq 2762  df-clel 2845  df-v 3464  df-un 3918  df-ss 3930  df-pr 4597  df-tp 4599

This theorem is referenced by:  fr3nr  7774  rngbase  17355  srngbase  17366  lmodbase  17382  ipsbase  17393  ipssca  17396  phlbase  17403  topgrpbas  17418  otpsbas  17433  odrngbas  17460  odrngtset  17463  prdssca  17512  prdsbas  17513  prdstset  17522  imasbas  17569  imassca  17576  imastset  17579  fucbas  18023  setcbas  18138  catcbas  18161  estrcbas  18184  cnfldbas  21509  cnfldtset  21515  psrbas  22067  psrsca  22080  trkgbas  28694  rlocbas  33558  rlocaddval  33559  rlocmulval  33560  idlsrgbas  33764  signswch  34918  algbase  43853  clsk1indlem4  44722  clsk1indlem1  44723  cycl3grtri  48661  rngcbasALTV  48980  ringcbasALTV  49014  catbas  49953  mndtcbasval  50307