Theorem 0elpw 5355

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 4397	. 2 ⊢ ∅ ⊆ 𝐴
2		0ex 5308	. . 3 ⊢ ∅ ∈ V
3	2	elpw 4607	. 2 ⊢ (∅ ∈ 𝒫 𝐴 ↔ ∅ ⊆ 𝐴)
4	1, 3	mpbir 230	1 ⊢ ∅ ∈ 𝒫 𝐴

Syntax hints:   ∈ wcel 2107   ⊆ wss 3949  ∅c0 4323  𝒫 cpw 4603

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704  ax-nul 5307

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-dif 3952  df-in 3956  df-ss 3966  df-nul 4324  df-pw 4605

This theorem is referenced by:  pwne0  5356  marypha1lem  9428  brwdom2  9568  canthwdom  9574  isfin1-3  10381  canthp1lem2  10648  ixxssxr  13336  incexc  15783  smupf  16419  hashbc0  16938  ramz2  16957  mreexexlem3d  17590  acsfn  17603  isdrs2  18259  fpwipodrs  18493  pwmndid  18817  pwmnd  18818  clsval2  22554  mretopd  22596  comppfsc  23036  alexsubALTlem2  23552  alexsubALTlem4  23554  0sno  27327  bday0s  27329  0slt1s  27330  bday0b  27331  madessno  27355  oldssno  27356  newssno  27357  lltropt  27367  made0  27368  eupth2lems  29491  esum0  33047  esumcst  33061  esumpcvgval  33076  prsiga  33129  pwldsys  33155  ldgenpisyslem1  33161  carsggect  33317  kur14  34207  0hf  35149  bj-tagss  35861  bj-0int  35982  bj-mooreset  35983  bj-ismoored0  35987  topdifinfindis  36227  0totbnd  36641  heiborlem6  36684  istopclsd  41438  ntrkbimka  42789  ntrk0kbimka  42790  clsk1indlem0  42792  ntrclscls00  42817  ntrneicls11  42841  ismnushort  43060  0pwfi  43746  dvnprodlem3  44664  pwsal  45031  salexct  45050  sge0rnn0  45084  sge00  45092  psmeasure  45187  caragen0  45222  0ome  45245  isomenndlem  45246  ovn0  45282  ovnsubadd2lem  45361  smfresal  45504  sprsymrelfvlem  46158  lincval0  47096  lco0  47108  linds0  47146