Theorem snelpwi 5383

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

Syntax hints:   → wi 4   ∈ wcel 2111  𝒫 cpw 4547  {csn 4573

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 2113  ax-9 2121  ax-ext 2703  ax-sep 5232  ax-pr 5368

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 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-un 3902  df-ss 3914  df-pw 4549  df-sn 4574  df-pr 4576

This theorem is referenced by:  unipw  5389  canth2  9043  pwfir  9201  unifpw  9239  marypha1lem  9317  infpwfidom  9919  ackbij1lem4  10113  acsfn  17565  sylow2a  19531  dissnref  23443  dissnlocfin  23444  locfindis  23445  txdis  23547  txdis1cn  23550  symgtgp  24021  1sno  27771  bday0s  27772  bday0b  27774  bday1s  27775  cutneg  27777  cutlt  27876  onscutlt  28201  n0sbday  28280  n0sfincut  28282  bdayn0p1  28294  zscut  28331  1p1e2s  28339  twocut  28346  addhalfcut  28379  dispcmp  33872  esumcst  34076  cntnevol  34241  coinflippvt  34498  onsucsuccmpi  36487  topdifinffinlem  37391  pclfinN  40009  lpirlnr  43220  unipwrVD  44934  unipwr  44935  salexct  46442  salexct3  46450  salgencntex  46451  salgensscntex  46452  sge0tsms  46488  sge0cl  46489  sge0sup  46499  isgrtri  48053  lincvalsng  48527  snlindsntor  48582