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

Theorem snelpwi 5329
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 4735 . 2 (𝐴𝐵 → {𝐴} ⊆ 𝐵)
2 snex 5324 . . 3 {𝐴} ∈ V
32elpw 4546 . 2 ({𝐴} ∈ 𝒫 𝐵 ↔ {𝐴} ⊆ 𝐵)
41, 3sylibr 236 1 (𝐴𝐵 → {𝐴} ∈ 𝒫 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2110  wss 3936  𝒫 cpw 4539  {csn 4561
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 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2156  ax-12 2172  ax-ext 2793  ax-sep 5196  ax-nul 5203  ax-pr 5322
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-v 3497  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-pw 4541  df-sn 4562  df-pr 4564
This theorem is referenced by:  unipw  5335  canth2  8664  unifpw  8821  marypha1lem  8891  infpwfidom  9448  ackbij1lem4  9639  acsfn  16924  sylow2a  18738  dissnref  22130  dissnlocfin  22131  locfindis  22132  txdis  22234  txdis1cn  22237  symgtgp  22708  dispcmp  31118  esumcst  31317  cntnevol  31482  coinflippvt  31737  onsucsuccmpi  33786  topdifinffinlem  34622  pclfinN  37030  lpirlnr  39710  unipwrVD  41159  unipwr  41160  salexct  42610  salexct3  42618  salgencntex  42619  salgensscntex  42620  sge0tsms  42655  sge0cl  42656  sge0sup  42666  lincvalsng  44464  snlindsntor  44519
  Copyright terms: Public domain W3C validator