Theorem snelpwi 5463

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

Syntax hints:   → wi 4   ∈ wcel 2108  𝒫 cpw 4622  {csn 4648

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711  ax-sep 5317  ax-pr 5447

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-un 3981  df-ss 3993  df-pw 4624  df-sn 4649  df-pr 4651

This theorem is referenced by:  unipw  5470  canth2  9196  pwfir  9383  unifpw  9425  marypha1lem  9502  infpwfidom  10097  ackbij1lem4  10291  acsfn  17717  sylow2a  19661  dissnref  23557  dissnlocfin  23558  locfindis  23559  txdis  23661  txdis1cn  23664  symgtgp  24135  1sno  27890  bday0s  27891  bday0b  27893  bday1s  27894  cutlt  27984  n0sbday  28372  zscut  28411  1p1e2s  28418  nohalf  28425  addhalfcut  28437  dispcmp  33805  esumcst  34027  cntnevol  34192  coinflippvt  34449  onsucsuccmpi  36409  topdifinffinlem  37313  pclfinN  39857  lpirlnr  43074  unipwrVD  44803  unipwr  44804  salexct  46255  salexct3  46263  salgencntex  46264  salgensscntex  46265  sge0tsms  46301  sge0cl  46302  sge0sup  46312  isgrtri  47794  lincvalsng  48145  snlindsntor  48200