Theorem 0elpw 4966

Description: Every power class contains the empty set. (Contributed by NM, 25-Oct-2007.)

Assertion

Ref	Expression
0elpw	⊢ ∅ ∈ 𝒫 𝐴

Proof of Theorem 0elpw

Step	Hyp	Ref	Expression
1		0ss 4117	. 2 ⊢ ∅ ⊆ 𝐴
2		0ex 4925	. . 3 ⊢ ∅ ∈ V
3	2	elpw 4304	. 2 ⊢ (∅ ∈ 𝒫 𝐴 ↔ ∅ ⊆ 𝐴)
4	1, 3	mpbir 221	1 ⊢ ∅ ∈ 𝒫 𝐴

Syntax hints:   ∈ wcel 2145   ⊆ wss 3723  ∅c0 4063  𝒫 cpw 4298

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-nul 4924

This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-v 3353  df-dif 3726  df-in 3730  df-ss 3737  df-nul 4064  df-pw 4300

This theorem is referenced by:  pwne0  4967  marypha1lem  8499  brwdom2  8638  canthwdom  8644  pwcdadom  9244  isfin1-3  9414  canthp1lem2  9681  ixxssxr  12392  incexc  14776  smupf  15408  hashbc0  15916  ramz2  15935  mreexexlem3d  16514  acsfn  16527  isdrs2  17147  fpwipodrs  17372  clsval2  21075  mretopd  21117  comppfsc  21556  alexsubALTlem2  22072  alexsubALTlem4  22074  eupth2lems  27418  esum0  30451  esumcst  30465  esumpcvgval  30480  prsiga  30534  pwldsys  30560  ldgenpisyslem1  30566  carsggect  30720  kur14  31536  0hf  32621  bj-tagss  33299  bj-0int  33387  bj-mooreset  33388  bj-ismoored0  33393  topdifinfindis  33531  0totbnd  33904  heiborlem6  33947  istopclsd  37789  ntrkbimka  38862  ntrk0kbimka  38863  clsk1indlem0  38865  ntrclscls00  38890  ntrneicls11  38914  0pwfi  39748  dvnprodlem3  40678  pwsal  41049  salexct  41066  sge0rnn0  41099  sge00  41107  psmeasure  41202  caragen0  41237  0ome  41260  isomenndlem  41261  ovn0  41297  ovnsubadd2lem  41376  smfresal  41512  sprsymrelfvlem  42265  lincval0  42729  lco0  42741  linds0  42779