Theorem snsspr1 4814

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 4178	. 2 ⊢ {𝐴} ⊆ ({𝐴} ∪ {𝐵})
2		df-pr 4629	. 2 ⊢ {𝐴, 𝐵} = ({𝐴} ∪ {𝐵})
3	1, 2	sseqtrri 4033	1 ⊢ {𝐴} ⊆ {𝐴, 𝐵}

Syntax hints:   ∪ cun 3949   ⊆ wss 3951  {csn 4626  {cpr 4628

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-un 3956  df-ss 3968  df-pr 4629

This theorem is referenced by:  snsstp1  4816  op1stb  5476  uniop  5520  1sdom2dom  9283  rankopb  9892  ltrelxr  11322  seqexw  14058  2strbas  17268  2strbas1  17272  phlvsca  17394  prdshom  17512  ipobas  18576  ipolerval  18577  gsumpr  19973  lspprid1  20995  lsppratlem3  21151  lsppratlem4  21152  ex-dif  30442  ex-un  30443  ex-in  30444  idlsrgtset  33536  coinflippv  34486  pthhashvtx  35133  subfacp1lem2a  35185  altopthsn  35962  rankaltopb  35980  dvh3dim3N  41451  mapdindp2  41723  lspindp5  41772  algsca  43189  clsk1indlem2  44055  clsk1indlem3  44056  clsk1indlem1  44058  mnuprdlem4  44294