Theorem snsspr1 4769

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-ss 3897  df-un 4150  df-pr 4587

This theorem is used by:  snsstp1  4771  op1stb  5440  uniop  5488  1sdom2dom  9252  rankopb  9873  ltrelxr  11377  seqexw  14167  2strbas  17415  phlvsca  17530  prdshom  17647  ipobas  18714  ipolerval  18715  chnccat  18809  gsumpr  20178  lspprid1  21281  lsppratlem3  21436  lsppratlem4  21437  pthhashvtx  30324  ex-dif  31033  ex-un  31034  ex-in  31035  idlsrgtset  34090  esplyind  34257  coinflippv  35166  subfacp1lem2a  36035  altopthsn  36822  rankaltopb  36840  dvh3dim3N  42615  mapdindp2  42887  lspindp5  42936  algsca  44288  clsk1indlem2  45151  clsk1indlem3  45152  clsk1indlem1  45154  mnuprdlem4  45368  setc1onsubc  50848