Theorem snelpwi 5454

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

Syntax hints:   → wi 4   ∈ wcel 2106  𝒫 cpw 4605  {csn 4631

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706  ax-sep 5302  ax-pr 5438

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1540  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-v 3480  df-un 3968  df-ss 3980  df-pw 4607  df-sn 4632  df-pr 4634

This theorem is referenced by:  unipw  5461  canth2  9169  pwfir  9353  unifpw  9393  marypha1lem  9471  infpwfidom  10066  ackbij1lem4  10260  acsfn  17704  sylow2a  19652  dissnref  23552  dissnlocfin  23553  locfindis  23554  txdis  23656  txdis1cn  23659  symgtgp  24130  1sno  27887  bday0s  27888  bday0b  27890  bday1s  27891  cutlt  27981  n0sbday  28369  zscut  28408  1p1e2s  28415  nohalf  28422  addhalfcut  28434  dispcmp  33820  esumcst  34044  cntnevol  34209  coinflippvt  34466  onsucsuccmpi  36426  topdifinffinlem  37330  pclfinN  39883  lpirlnr  43106  unipwrVD  44830  unipwr  44831  salexct  46290  salexct3  46298  salgencntex  46299  salgensscntex  46300  sge0tsms  46336  sge0cl  46337  sge0sup  46347  isgrtri  47848  lincvalsng  48262  snlindsntor  48317