Theorem snssd 3763

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

Syntax hints:   → wi 4   ↔ wb 105   ∈ wcel 2164   ⊆ wss 3153  {csn 3618

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 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-nfc 2325  df-v 2762  df-in 3159  df-ss 3166  df-sn 3624

This theorem is referenced by:  pwntru  4228  ecinxp  6664  xpdom3m  6888  ac6sfi  6954  undifdc  6980  iunfidisj  7005  fidcenumlemr  7014  ssfii  7033  en2other2  7256  un0addcl  9273  un0mulcl  9274  fseq1p1m1  10160  fsumge1  11604  fprodsplit1f  11777  phicl2  12352  ennnfonelemhf1o  12570  imasaddfnlemg  12897  imasaddflemg  12899  0subm  13056  gsumvallem2  13065  trivsubgd  13270  trivsubgsnd  13271  trivnsgd  13287  kerf1ghm  13344  lsssn0  13866  lss0ss  13867  lsptpcl  13890  lspsnvsi  13914  lspun0  13921  mulgrhm2  14098  zndvds  14137  rest0  14347  iscnp4  14386  cnconst2  14401  cnpdis  14410  txdis  14445  txdis1cn  14446  fsumcncntop  14724  dvef  14873  plyf  14883  elplyr  14886  elplyd  14887  ply1term  14889  plyaddlem  14895  plymullem  14896  bj-omtrans  15448  pwtrufal  15488