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

Theorem 0elpw 4804
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 3950 . 2 ∅ ⊆ 𝐴
2 0ex 4760 . . 3 ∅ ∈ V
32elpw 4142 . 2 (∅ ∈ 𝒫 𝐴 ↔ ∅ ⊆ 𝐴)
41, 3mpbir 221 1 ∅ ∈ 𝒫 𝐴
Colors of variables: wff setvar class
Syntax hints:  wcel 1987  wss 3560  c0 3897  𝒫 cpw 4136
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-nul 4759
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-v 3192  df-dif 3563  df-in 3567  df-ss 3574  df-nul 3898  df-pw 4138
This theorem is referenced by:  pwne0  4805  marypha1lem  8299  brwdom2  8438  canthwdom  8444  pwcdadom  8998  isfin1-3  9168  canthp1lem2  9435  ixxssxr  12145  incexc  14513  smupf  15143  hashbc0  15652  ramz2  15671  mreexexlem3d  16246  acsfn  16260  isdrs2  16879  fpwipodrs  17104  clsval2  20794  mretopd  20836  comppfsc  21275  alexsubALTlem2  21792  alexsubALTlem4  21794  eupth2lems  26998  esum0  29934  esumcst  29948  esumpcvgval  29963  prsiga  30017  pwldsys  30043  ldgenpisyslem1  30049  carsggect  30203  kur14  30959  0hf  31979  bj-tagss  32668  topdifinfindis  32865  0totbnd  33243  heiborlem6  33286  istopclsd  36782  ntrkbimka  37857  ntrk0kbimka  37858  clsk1indlem0  37860  ntrclscls00  37885  ntrneicls11  37909  0pwfi  38749  dvnprodlem3  39500  pwsal  39872  salexct  39889  sge0rnn0  39922  sge00  39930  psmeasure  40025  caragen0  40057  0ome  40080  isomenndlem  40081  ovn0  40117  ovnsubadd2lem  40196  smfresal  40332  sprsymrelfvlem  41058  lincval0  41522  lco0  41534  linds0  41572
  Copyright terms: Public domain W3C validator