Theorem snsspr1 4775

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

This proof depends on syntax axioms:   ∪ cun 3897   ⊆ wss 3899  {csn 4584  {cpr 4586

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-un 3904  df-ss 3916  df-pr 4587

This theorem is used by:  snsstp1  4777  op1stb  5447  uniop  5492  1sdom2dom  9224  rankopb  9834  ltrelxr  11294  seqexw  14081  2strbas  17320  phlvsca  17435  prdshom  17552  ipobas  18619  ipolerval  18620  chnccat  18714  gsumpr  20082  lspprid1  21181  lsppratlem3  21336  lsppratlem4  21337  pthhashvtx  30194  ex-dif  30903  ex-un  30904  ex-in  30905  idlsrgtset  33918  esplyind  34085  coinflippv  34995  subfacp1lem2a  35759  altopthsn  36541  rankaltopb  36559  dvh3dim3N  42322  mapdindp2  42594  lspindp5  42643  algsca  44018  clsk1indlem2  44882  clsk1indlem3  44883  clsk1indlem1  44885  mnuprdlem4  45099  setc1onsubc  50528