Theorem snsspr1 4749

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

Syntax hints:   ∪ cun 3936   ⊆ wss 3938  {csn 4569  {cpr 4571

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-v 3498  df-un 3943  df-in 3945  df-ss 3954  df-pr 4572

This theorem is referenced by:  snsstp1  4751  op1stb  5365  uniop  5407  rankopb  9283  ltrelxr  10704  seqexw  13388  2strbas  16605  2strbas1  16608  phlvsca  16659  prdshom  16742  ipobas  17767  ipolerval  17768  gsumpr  19077  lspprid1  19771  lsppratlem3  19923  lsppratlem4  19924  ex-dif  28204  ex-un  28205  ex-in  28206  coinflippv  31743  pthhashvtx  32376  subfacp1lem2a  32429  altopthsn  33424  rankaltopb  33442  dvh3dim3N  38587  mapdindp2  38859  lspindp5  38908  algsca  39788  clsk1indlem2  40399  clsk1indlem3  40400  clsk1indlem1  40402  mnuprdlem4  40618