Theorem snelpwi 5360

Description: A singleton of a set belongs to the power class of a class containing the set. (Contributed by Alan Sare, 25-Aug-2011.)

Assertion

Ref	Expression
snelpwi	⊢ (𝐴 ∈ 𝐵 → {𝐴} ∈ 𝒫 𝐵)

Proof of Theorem snelpwi

Step	Hyp	Ref	Expression
1		snssi 4741	. 2 ⊢ (𝐴 ∈ 𝐵 → {𝐴} ⊆ 𝐵)
2		snex 5354	. . 3 ⊢ {𝐴} ∈ V
3	2	elpw 4537	. 2 ⊢ ({𝐴} ∈ 𝒫 𝐵 ↔ {𝐴} ⊆ 𝐵)
4	1, 3	sylibr 233	1 ⊢ (𝐴 ∈ 𝐵 → {𝐴} ∈ 𝒫 𝐵)

Syntax hints:   → wi 4   ∈ wcel 2106   ⊆ wss 3887  𝒫 cpw 4533  {csn 4561

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709  ax-sep 5223  ax-nul 5230  ax-pr 5352

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3434  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-pw 4535  df-sn 4562  df-pr 4564

This theorem is referenced by:  unipw  5366  canth2  8917  pwfir  8959  unifpw  9122  marypha1lem  9192  infpwfidom  9784  ackbij1lem4  9979  acsfn  17368  sylow2a  19224  dissnref  22679  dissnlocfin  22680  locfindis  22681  txdis  22783  txdis1cn  22786  symgtgp  23257  dispcmp  31809  esumcst  32031  cntnevol  32196  coinflippvt  32451  1sno  34021  bday0s  34022  bday0b  34024  bday1s  34025  onsucsuccmpi  34632  topdifinffinlem  35518  pclfinN  37914  lpirlnr  40942  unipwrVD  42452  unipwr  42453  salexct  43873  salexct3  43881  salgencntex  43882  salgensscntex  43883  sge0tsms  43918  sge0cl  43919  sge0sup  43929  lincvalsng  45757  snlindsntor  45812