Theorem snelpwi 5354

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 4738	. 2 ⊢ (𝐴 ∈ 𝐵 → {𝐴} ⊆ 𝐵)
2		snex 5349	. . 3 ⊢ {𝐴} ∈ V
3	2	elpw 4534	. 2 ⊢ ({𝐴} ∈ 𝒫 𝐵 ↔ {𝐴} ⊆ 𝐵)
4	1, 3	sylibr 233	1 ⊢ (𝐴 ∈ 𝐵 → {𝐴} ∈ 𝒫 𝐵)

Syntax hints:   → wi 4   ∈ wcel 2108   ⊆ wss 3883  𝒫 cpw 4530  {csn 4558

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pr 5347

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-pw 4532  df-sn 4559  df-pr 4561

This theorem is referenced by:  unipw  5360  canth2  8866  pwfir  8921  unifpw  9052  marypha1lem  9122  infpwfidom  9715  ackbij1lem4  9910  acsfn  17285  sylow2a  19139  dissnref  22587  dissnlocfin  22588  locfindis  22589  txdis  22691  txdis1cn  22694  symgtgp  23165  dispcmp  31711  esumcst  31931  cntnevol  32096  coinflippvt  32351  1sno  33948  bday0s  33949  bday0b  33951  bday1s  33952  onsucsuccmpi  34559  topdifinffinlem  35445  pclfinN  37841  lpirlnr  40858  unipwrVD  42341  unipwr  42342  salexct  43763  salexct3  43771  salgencntex  43772  salgensscntex  43773  sge0tsms  43808  sge0cl  43809  sge0sup  43819  lincvalsng  45645  snlindsntor  45700