Theorem snelpwi 5398

Description: If a set is a member of a class, then the singleton of that set is a member of the powerclass of that class. (Contributed by Alan Sare, 25-Aug-2011.)

Assertion

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

Proof of Theorem snelpwi

Step	Hyp	Ref	Expression
1		snelpwg 5397	. 2 ⊢ (𝐴 ∈ 𝐵 → (𝐴 ∈ 𝐵 ↔ {𝐴} ∈ 𝒫 𝐵))
2	1	ibi 267	1 ⊢ (𝐴 ∈ 𝐵 → {𝐴} ∈ 𝒫 𝐵)

Syntax hints:   → wi 4   ∈ wcel 2109  𝒫 cpw 4559  {csn 4585

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5246  ax-pr 5382

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3446  df-un 3916  df-ss 3928  df-pw 4561  df-sn 4586  df-pr 4588

This theorem is referenced by:  unipw  5405  canth2  9071  pwfir  9242  unifpw  9282  marypha1lem  9360  infpwfidom  9957  ackbij1lem4  10151  acsfn  17596  sylow2a  19525  dissnref  23391  dissnlocfin  23392  locfindis  23393  txdis  23495  txdis1cn  23498  symgtgp  23969  1sno  27715  bday0s  27716  bday0b  27718  bday1s  27719  cutneg  27721  cutlt  27816  onscutlt  28141  n0sbday  28220  n0sfincut  28222  bdayn0p1  28234  zscut  28271  1p1e2s  28278  twocut  28285  addhalfcut  28310  dispcmp  33822  esumcst  34026  cntnevol  34191  coinflippvt  34449  onsucsuccmpi  36404  topdifinffinlem  37308  pclfinN  39867  lpirlnr  43079  unipwrVD  44794  unipwr  44795  salexct  46305  salexct3  46313  salgencntex  46314  salgensscntex  46315  sge0tsms  46351  sge0cl  46352  sge0sup  46362  isgrtri  47915  lincvalsng  48378  snlindsntor  48433