Theorem snelpwi 5403

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

Syntax hints:   → wi 4   ∈ wcel 2109  𝒫 cpw 4563  {csn 4589

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 5251  ax-pr 5387

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 3449  df-un 3919  df-ss 3931  df-pw 4565  df-sn 4590  df-pr 4592

This theorem is referenced by:  unipw  5410  canth2  9094  pwfir  9266  unifpw  9306  marypha1lem  9384  infpwfidom  9981  ackbij1lem4  10175  acsfn  17620  sylow2a  19549  dissnref  23415  dissnlocfin  23416  locfindis  23417  txdis  23519  txdis1cn  23522  symgtgp  23993  1sno  27739  bday0s  27740  bday0b  27742  bday1s  27743  cutneg  27745  cutlt  27840  onscutlt  28165  n0sbday  28244  n0sfincut  28246  bdayn0p1  28258  zscut  28295  1p1e2s  28302  twocut  28309  addhalfcut  28334  dispcmp  33849  esumcst  34053  cntnevol  34218  coinflippvt  34476  onsucsuccmpi  36431  topdifinffinlem  37335  pclfinN  39894  lpirlnr  43106  unipwrVD  44821  unipwr  44822  salexct  46332  salexct3  46340  salgencntex  46341  salgensscntex  46342  sge0tsms  46378  sge0cl  46379  sge0sup  46389  isgrtri  47942  lincvalsng  48405  snlindsntor  48460