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  11714  fprodsplit1f  11887  bitsinv1  12215  phicl2  12478  ennnfonelemhf1o  12726  imasaddfnlemg  13088  imasaddflemg  13090  0subm  13258  gsumvallem2  13267  trivsubgd  13478  trivsubgsnd  13479  trivnsgd  13495  kerf1ghm  13552  lsssn0  14074  lss0ss  14075  lsptpcl  14098  lspsnvsi  14122  lspun0  14129  mulgrhm2  14314  zndvds  14353  rest0  14593  iscnp4  14632  cnconst2  14647  cnpdis  14656  txdis  14691  txdis1cn  14692  fsumcncntop  14981  dvef  15141  plyf  15151  elplyr  15154  elplyd  15155  ply1term  15157  plyaddlem  15163  plymullem  15164  plycolemc  15172  plycn  15176  dvply2g  15180  perfectlem2  15414  bj-omtrans  15825  pwtrufal  15867