Theorem snelpwi 5392

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

Syntax hints:   → wi 4   ∈ wcel 2113  𝒫 cpw 4554  {csn 4580

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708  ax-sep 5241  ax-pr 5377

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-un 3906  df-ss 3918  df-pw 4556  df-sn 4581  df-pr 4583

This theorem is referenced by:  unipw  5398  canth2  9058  pwfir  9217  unifpw  9255  marypha1lem  9336  infpwfidom  9938  ackbij1lem4  10132  acsfn  17582  sylow2a  19548  dissnref  23472  dissnlocfin  23473  locfindis  23474  txdis  23576  txdis1cn  23579  symgtgp  24050  1no  27806  bday0  27807  bday0b  27809  bday1  27810  cutneg  27812  cutlt  27928  oncutlt  28260  n0bday  28348  n0fincut  28351  bdayn0p1  28365  zcuts  28403  twocut  28419  addhalfcut  28455  dispcmp  34016  esumcst  34220  cntnevol  34385  coinflippvt  34642  onsucsuccmpi  36637  topdifinffinlem  37552  pclfinN  40160  lpirlnr  43359  unipwrVD  45072  unipwr  45073  salexct  46578  salexct3  46586  salgencntex  46587  salgensscntex  46588  sge0tsms  46624  sge0cl  46625  sge0sup  46635  isgrtri  48189  lincvalsng  48662  snlindsntor  48717