Theorem snssd 3860

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 105   ∈ wcel 2209   ⊆ wss 3220  {csn 3709

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-v 2823  df-in 3226  df-ss 3233  df-sn 3715

This theorem is used by:  pwntru  4336  ecinxp  6884  xpdom3m  7132  ac6sfi  7202  undifdc  7231  iunfidisj  7260  fidcenumlemr  7272  ssfii  7308  en2other2  7548  pw1m  7583  un0addcl  9600  un0mulcl  9601  fseq1p1m1  10511  hashfibclem  11296  hashf1lem1  11299  hashf1lem2  11300  fsumge1  12244  fprodsplit1f  12417  bitsinv1  12745  phicl2  13012  ennnfonelemhf1o  13353  imasaddfnlemg  13684  imasaddflemg  13686  0subm  13840  gsumvallem2  13849  trivsubgd  14052  trivsubgsnd  14053  trivnsgd  14069  kerf1ghm  14126  gsumclfi  14208  gsummptfidmadd  14210  gsumsubmclfi  14212  lsssn0  14756  lss0ss  14757  lsptpcl  14780  lspsnvsi  14804  lspun0  14811  mulgrhm2  14994  zndvds  15033  rest0  15329  iscnp4  15368  cnconst2  15383  cnpdis  15392  txdis  15427  txdis1cn  15428  fsumcncntop  15717  dvef  15877  plyf  15887  elplyr  15890  elplyd  15891  ply1term  15893  plyaddlem  15899  plymullem  15900  plycolemc  15908  plycn  15912  dvply2g  15916  ppiprm  16170  perfectlem2  16198  upgr1elem1  16459  bj-omtrans  17080  pwtrufal  17125