Theorem snssd 3768

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 3757	. . 3 ⊢ (𝐴 ∈ 𝐵 → (𝐴 ∈ 𝐵 ↔ {𝐴} ⊆ 𝐵))
3	1, 2	syl 14	. 2 ⊢ (𝜑 → (𝐴 ∈ 𝐵 ↔ {𝐴} ⊆ 𝐵))
4	1, 3	mpbid 147	1 ⊢ (𝜑 → {𝐴} ⊆ 𝐵)

Syntax hints:   → wi 4   ↔ wb 105   ∈ wcel 2167   ⊆ wss 3157  {csn 3623

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 710  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-v 2765  df-in 3163  df-ss 3170  df-sn 3629

This theorem is referenced by:  pwntru  4233  ecinxp  6678  xpdom3m  6902  ac6sfi  6968  undifdc  6994  iunfidisj  7021  fidcenumlemr  7030  ssfii  7049  en2other2  7277  un0addcl  9301  un0mulcl  9302  fseq1p1m1  10188  fsumge1  11645  fprodsplit1f  11818  bitsinv1  12146  phicl2  12409  ennnfonelemhf1o  12657  imasaddfnlemg  13018  imasaddflemg  13020  0subm  13188  gsumvallem2  13197  trivsubgd  13408  trivsubgsnd  13409  trivnsgd  13425  kerf1ghm  13482  lsssn0  14004  lss0ss  14005  lsptpcl  14028  lspsnvsi  14052  lspun0  14059  mulgrhm2  14244  zndvds  14283  rest0  14523  iscnp4  14562  cnconst2  14577  cnpdis  14586  txdis  14621  txdis1cn  14622  fsumcncntop  14911  dvef  15071  plyf  15081  elplyr  15084  elplyd  15085  ply1term  15087  plyaddlem  15093  plymullem  15094  plycolemc  15102  plycn  15106  dvply2g  15110  perfectlem2  15344  bj-omtrans  15710  pwtrufal  15752