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 2114  𝒫 cpw 4542  {csn 4568

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5232  ax-pr 5371

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3432  df-un 3895  df-ss 3907  df-pw 4544  df-sn 4569  df-pr 4571

This theorem is referenced by:  unipw  5398  canth2  9062  pwfir  9221  unifpw  9259  marypha1lem  9340  infpwfidom  9944  ackbij1lem4  10138  acsfn  17619  sylow2a  19588  dissnref  23506  dissnlocfin  23507  locfindis  23508  txdis  23610  txdis1cn  23613  symgtgp  24084  1no  27819  bday0  27820  bday0b  27822  bday1  27823  cutneg  27825  cutlt  27941  oncutlt  28273  n0bday  28361  n0fincut  28364  bdayn0p1  28378  zcuts  28416  twocut  28432  addhalfcut  28468  dispcmp  34022  esumcst  34226  cntnevol  34391  coinflippvt  34648  onsucsuccmpi  36644  topdifinffinlem  37680  pclfinN  40363  lpirlnr  43566  unipwrVD  45279  unipwr  45280  salexct  46783  salexct3  46791  salgencntex  46792  salgensscntex  46793  sge0tsms  46829  sge0cl  46830  sge0sup  46840  isgrtri  48434  lincvalsng  48907  snlindsntor  48962