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  17600  sylow2a  19533  dissnref  23448  dissnlocfin  23449  locfindis  23450  txdis  23552  txdis1cn  23555  symgtgp  24026  1sno  27776  bday0s  27777  bday0b  27779  bday1s  27780  cutneg  27782  cutlt  27880  onscutlt  28205  n0sbday  28284  n0sfincut  28286  bdayn0p1  28298  zscut  28335  1p1e2s  28343  twocut  28350  addhalfcut  28382  dispcmp  33842  esumcst  34046  cntnevol  34211  coinflippvt  34469  onsucsuccmpi  36424  topdifinffinlem  37328  pclfinN  39887  lpirlnr  43099  unipwrVD  44814  unipwr  44815  salexct  46325  salexct3  46333  salgencntex  46334  salgensscntex  46335  sge0tsms  46371  sge0cl  46372  sge0sup  46382  isgrtri  47935  lincvalsng  48398  snlindsntor  48453