Theorem snelpwi 5448

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 5447	. 2 ⊢ (𝐴 ∈ 𝐵 → (𝐴 ∈ 𝐵 ↔ {𝐴} ∈ 𝒫 𝐵))
2	1	ibi 267	1 ⊢ (𝐴 ∈ 𝐵 → {𝐴} ∈ 𝒫 𝐵)

Syntax hints:   → wi 4   ∈ wcel 2108  𝒫 cpw 4600  {csn 4626

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-sep 5296  ax-pr 5432

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-un 3956  df-ss 3968  df-pw 4602  df-sn 4627  df-pr 4629

This theorem is referenced by:  unipw  5455  canth2  9170  pwfir  9355  unifpw  9395  marypha1lem  9473  infpwfidom  10068  ackbij1lem4  10262  acsfn  17702  sylow2a  19637  dissnref  23536  dissnlocfin  23537  locfindis  23538  txdis  23640  txdis1cn  23643  symgtgp  24114  1sno  27872  bday0s  27873  bday0b  27875  bday1s  27876  cutlt  27966  n0sbday  28354  zscut  28393  1p1e2s  28400  nohalf  28407  addhalfcut  28419  dispcmp  33858  esumcst  34064  cntnevol  34229  coinflippvt  34487  onsucsuccmpi  36444  topdifinffinlem  37348  pclfinN  39902  lpirlnr  43129  unipwrVD  44852  unipwr  44853  salexct  46349  salexct3  46357  salgencntex  46358  salgensscntex  46359  sge0tsms  46395  sge0cl  46396  sge0sup  46406  isgrtri  47910  lincvalsng  48333  snlindsntor  48388