MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  snelpwi Structured version   Visualization version   GIF version

Theorem snelpwi 5344
Description: A singleton of a set belongs to the power class of a class containing the set. (Contributed by Alan Sare, 25-Aug-2011.)
Assertion
Ref Expression
snelpwi (𝐴𝐵 → {𝐴} ∈ 𝒫 𝐵)

Proof of Theorem snelpwi
StepHypRef Expression
1 snssi 4736 . 2 (𝐴𝐵 → {𝐴} ⊆ 𝐵)
2 snex 5339 . . 3 {𝐴} ∈ V
32elpw 4532 . 2 ({𝐴} ∈ 𝒫 𝐵 ↔ {𝐴} ⊆ 𝐵)
41, 3sylibr 237 1 (𝐴𝐵 → {𝐴} ∈ 𝒫 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2111  wss 3881  𝒫 cpw 4528  {csn 4556
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2113  ax-9 2121  ax-ext 2709  ax-sep 5207  ax-nul 5214  ax-pr 5337
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-tru 1546  df-fal 1556  df-ex 1788  df-sb 2072  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3423  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-nul 4253  df-pw 4530  df-sn 4557  df-pr 4559
This theorem is referenced by:  unipw  5350  canth2  8822  pwfir  8877  unifpw  9004  marypha1lem  9074  infpwfidom  9667  ackbij1lem4  9862  acsfn  17187  sylow2a  19033  dissnref  22449  dissnlocfin  22450  locfindis  22451  txdis  22553  txdis1cn  22556  symgtgp  23027  dispcmp  31547  esumcst  31767  cntnevol  31932  coinflippvt  32187  1sno  33784  bday0s  33785  bday0b  33787  bday1s  33788  onsucsuccmpi  34395  topdifinffinlem  35282  pclfinN  37678  lpirlnr  40674  unipwrVD  42154  unipwr  42155  salexct  43577  salexct3  43585  salgencntex  43586  salgensscntex  43587  sge0tsms  43622  sge0cl  43623  sge0sup  43633  lincvalsng  45459  snlindsntor  45514
  Copyright terms: Public domain W3C validator