Theorem snelpwi 5390

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

Syntax hints:   → wi 4   ∈ wcel 2113  𝒫 cpw 4552  {csn 4578

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 2706  ax-sep 5239  ax-pr 5375

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 2713  df-cleq 2726  df-clel 2809  df-v 3440  df-un 3904  df-ss 3916  df-pw 4554  df-sn 4579  df-pr 4581

This theorem is referenced by:  unipw  5396  canth2  9056  pwfir  9215  unifpw  9253  marypha1lem  9334  infpwfidom  9936  ackbij1lem4  10130  acsfn  17580  sylow2a  19546  dissnref  23470  dissnlocfin  23471  locfindis  23472  txdis  23574  txdis1cn  23577  symgtgp  24048  1sno  27798  bday0s  27799  bday0b  27801  bday1s  27802  cutneg  27804  cutlt  27903  onscutlt  28232  n0sbday  28312  n0sfincut  28315  bdayn0p1  28327  zscut  28365  1p1e2s  28374  twocut  28381  addhalfcut  28416  dispcmp  33965  esumcst  34169  cntnevol  34334  coinflippvt  34591  onsucsuccmpi  36586  topdifinffinlem  37491  pclfinN  40099  lpirlnr  43301  unipwrVD  45014  unipwr  45015  salexct  46520  salexct3  46528  salgencntex  46529  salgensscntex  46530  sge0tsms  46566  sge0cl  46567  sge0sup  46577  isgrtri  48131  lincvalsng  48604  snlindsntor  48659