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

Theorem 0elpw 5247
Description: Every power class contains the empty set. (Contributed by NM, 25-Oct-2007.)
Assertion
Ref Expression
0elpw ∅ ∈ 𝒫 𝐴

Proof of Theorem 0elpw
StepHypRef Expression
1 0ss 4347 . 2 ∅ ⊆ 𝐴
2 0ex 5202 . . 3 ∅ ∈ V
32elpw 4542 . 2 (∅ ∈ 𝒫 𝐴 ↔ ∅ ⊆ 𝐴)
41, 3mpbir 232 1 ∅ ∈ 𝒫 𝐴
Colors of variables: wff setvar class
Syntax hints:  wcel 2105  wss 3933  c0 4288  𝒫 cpw 4535
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-nul 5201
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-v 3494  df-dif 3936  df-in 3940  df-ss 3949  df-nul 4289  df-pw 4537
This theorem is referenced by:  pwne0  5248  marypha1lem  8885  brwdom2  9025  canthwdom  9031  isfin1-3  9796  canthp1lem2  10063  ixxssxr  12738  incexc  15180  smupf  15815  hashbc0  16329  ramz2  16348  mreexexlem3d  16905  acsfn  16918  isdrs2  17537  fpwipodrs  17762  pwmndid  18039  pwmnd  18040  clsval2  21586  mretopd  21628  comppfsc  22068  alexsubALTlem2  22584  alexsubALTlem4  22586  eupth2lems  27944  esum0  31207  esumcst  31221  esumpcvgval  31236  prsiga  31289  pwldsys  31315  ldgenpisyslem1  31321  carsggect  31475  kur14  32360  0hf  33535  bj-tagss  34189  bj-0int  34287  bj-mooreset  34288  bj-ismoored0  34292  topdifinfindis  34509  0totbnd  34932  heiborlem6  34975  istopclsd  39175  ntrkbimka  40266  ntrk0kbimka  40267  clsk1indlem0  40269  ntrclscls00  40294  ntrneicls11  40318  0pwfi  41198  dvnprodlem3  42109  pwsal  42477  salexct  42494  sge0rnn0  42527  sge00  42535  psmeasure  42630  caragen0  42665  0ome  42688  isomenndlem  42689  ovn0  42725  ovnsubadd2lem  42804  smfresal  42940  sprsymrelfvlem  43529  lincval0  44398  lco0  44410  linds0  44448
  Copyright terms: Public domain W3C validator