Theorem snsspr1 4774

Description: A singleton is a subset of an unordered pair containing its member. (Contributed by NM, 27-Aug-2004.)

Assertion

Ref	Expression
snsspr1	⊢ {𝐴} ⊆ {𝐴, 𝐵}

Proof of Theorem snsspr1

Step	Hyp	Ref	Expression
1		ssun1 4137	. 2 ⊢ {𝐴} ⊆ ({𝐴} ∪ {𝐵})
2		df-pr 4588	. 2 ⊢ {𝐴, 𝐵} = ({𝐴} ∪ {𝐵})
3	1, 2	sseqtrri 3993	1 ⊢ {𝐴} ⊆ {𝐴, 𝐵}

Syntax hints:   ∪ cun 3909   ⊆ wss 3911  {csn 4585  {cpr 4587

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 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3446  df-un 3916  df-ss 3928  df-pr 4588

This theorem is referenced by:  snsstp1  4776  op1stb  5426  uniop  5470  1sdom2dom  9170  rankopb  9781  ltrelxr  11211  seqexw  13958  2strbas  17174  phlvsca  17289  prdshom  17406  ipobas  18466  ipolerval  18467  gsumpr  19861  lspprid1  20879  lsppratlem3  21035  lsppratlem4  21036  ex-dif  30325  ex-un  30326  ex-in  30327  idlsrgtset  33452  coinflippv  34448  pthhashvtx  35088  subfacp1lem2a  35140  altopthsn  35922  rankaltopb  35940  dvh3dim3N  41416  mapdindp2  41688  lspindp5  41737  algsca  43139  clsk1indlem2  44004  clsk1indlem3  44005  clsk1indlem1  44007  mnuprdlem4  44237  setc1onsubc  49564