Theorem snssd 3844

Description: The singleton of an element of a class is a subset of the class (deduction form). (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)

Hypothesis

Ref	Expression
snssd.1	⊢ (𝜑 → 𝐴 ∈ 𝐵)

Assertion

Ref	Expression
snssd	⊢ (𝜑 → {𝐴} ⊆ 𝐵)

Proof of Theorem snssd

Step	Hyp	Ref	Expression
1		snssd.1	. 2 ⊢ (𝜑 → 𝐴 ∈ 𝐵)
2		snssg 3833	. . 3 ⊢ (𝐴 ∈ 𝐵 → (𝐴 ∈ 𝐵 ↔ {𝐴} ⊆ 𝐵))
3	1, 2	syl 14	. 2 ⊢ (𝜑 → (𝐴 ∈ 𝐵 ↔ {𝐴} ⊆ 𝐵))
4	1, 3	mpbid 147	1 ⊢ (𝜑 → {𝐴} ⊆ 𝐵)

Syntax hints:   → wi 4   ↔ wb 105   ∈ wcel 2205   ⊆ wss 3214  {csn 3694

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-v 2817  df-in 3220  df-ss 3227  df-sn 3700

This theorem is referenced by:  pwntru  4317  ecinxp  6857  xpdom3m  7098  ac6sfi  7168  undifdc  7197  iunfidisj  7226  fidcenumlemr  7238  ssfii  7274  en2other2  7512  pw1m  7547  un0addcl  9546  un0mulcl  9547  fseq1p1m1  10450  hashfibclem  11231  fsumge1  12172  fprodsplit1f  12345  bitsinv1  12673  phicl2  12936  ennnfonelemhf1o  13248  imasaddfnlemg  13578  imasaddflemg  13580  0subm  13739  gsumvallem2  13748  trivsubgd  13953  trivsubgsnd  13954  trivnsgd  13970  kerf1ghm  14027  gfsumcl  14110  lsssn0  14644  lss0ss  14645  lsptpcl  14668  lspsnvsi  14692  lspun0  14699  mulgrhm2  14884  zndvds  14923  rest0  15170  iscnp4  15209  cnconst2  15224  cnpdis  15233  txdis  15268  txdis1cn  15269  fsumcncntop  15558  dvef  15718  plyf  15728  elplyr  15731  elplyd  15732  ply1term  15734  plyaddlem  15740  plymullem  15741  plycolemc  15749  plycn  15753  dvply2g  15757  perfectlem2  15994  upgr1elem1  16241  bj-omtrans  16852  pwtrufal  16897