Theorem snelpwi 5302

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 4701	. 2 ⊢ (𝐴 ∈ 𝐵 → {𝐴} ⊆ 𝐵)
2		snex 5297	. . 3 ⊢ {𝐴} ∈ V
3	2	elpw 4501	. 2 ⊢ ({𝐴} ∈ 𝒫 𝐵 ↔ {𝐴} ⊆ 𝐵)
4	1, 3	sylibr 237	1 ⊢ (𝐴 ∈ 𝐵 → {𝐴} ∈ 𝒫 𝐵)

Syntax hints:   → wi 4   ∈ wcel 2111   ⊆ wss 3881  𝒫 cpw 4497  {csn 4525

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-12 2175  ax-ext 2770  ax-sep 5167  ax-nul 5174  ax-pr 5295

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-nul 4244  df-pw 4499  df-sn 4526  df-pr 4528

This theorem is referenced by:  unipw  5308  canth2  8654  unifpw  8811  marypha1lem  8881  infpwfidom  9439  ackbij1lem4  9634  acsfn  16922  sylow2a  18736  dissnref  22133  dissnlocfin  22134  locfindis  22135  txdis  22237  txdis1cn  22240  symgtgp  22711  dispcmp  31212  esumcst  31432  cntnevol  31597  coinflippvt  31852  onsucsuccmpi  33904  topdifinffinlem  34764  pclfinN  37196  lpirlnr  40061  unipwrVD  41538  unipwr  41539  salexct  42974  salexct3  42982  salgencntex  42983  salgensscntex  42984  sge0tsms  43019  sge0cl  43020  sge0sup  43030  lincvalsng  44825  snlindsntor  44880