Theorem snssd 3777

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

Syntax hints:   → wi 4   ↔ wb 105   ∈ wcel 2175   ⊆ wss 3165  {csn 3632

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 1469  ax-7 1470  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-8 1526  ax-10 1527  ax-11 1528  ax-i12 1529  ax-bndl 1531  ax-4 1532  ax-17 1548  ax-i9 1552  ax-ial 1556  ax-i5r 1557  ax-ext 2186

This theorem depends on definitions:  df-bi 117  df-tru 1375  df-nf 1483  df-sb 1785  df-clab 2191  df-cleq 2197  df-clel 2200  df-nfc 2336  df-v 2773  df-in 3171  df-ss 3178  df-sn 3638

This theorem is referenced by:  pwntru  4242  ecinxp  6696  xpdom3m  6928  ac6sfi  6994  undifdc  7020  iunfidisj  7047  fidcenumlemr  7056  ssfii  7075  en2other2  7303  un0addcl  9327  un0mulcl  9328  fseq1p1m1  10215  fsumge1  11743  fprodsplit1f  11916  bitsinv1  12244  phicl2  12507  ennnfonelemhf1o  12755  imasaddfnlemg  13117  imasaddflemg  13119  0subm  13287  gsumvallem2  13296  trivsubgd  13507  trivsubgsnd  13508  trivnsgd  13524  kerf1ghm  13581  lsssn0  14103  lss0ss  14104  lsptpcl  14127  lspsnvsi  14151  lspun0  14158  mulgrhm2  14343  zndvds  14382  rest0  14622  iscnp4  14661  cnconst2  14676  cnpdis  14685  txdis  14720  txdis1cn  14721  fsumcncntop  15010  dvef  15170  plyf  15180  elplyr  15183  elplyd  15184  ply1term  15186  plyaddlem  15192  plymullem  15193  plycolemc  15201  plycn  15205  dvply2g  15209  perfectlem2  15443  bj-omtrans  15854  pwtrufal  15896