Theorem 0elpw 5291

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 4335	. 2 ⊢ ∅ ⊆ 𝐴
2		0ex 5236	. . 3 ⊢ ∅ ∈ V
3	2	elpw 4540	. 2 ⊢ (∅ ∈ 𝒫 𝐴 ↔ ∅ ⊆ 𝐴)
4	1, 3	mpbir 232	1 ⊢ ∅ ∈ 𝒫 𝐴

Syntax hints:   ∈ wcel 2119   ⊆ wss 3890  ∅c0 4268  𝒫 cpw 4536

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712  ax-nul 5235

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-v 3434  df-dif 3893  df-ss 3907  df-nul 4269  df-pw 4538

This theorem is referenced by:  pwne0  5292  marypha1lem  9343  brwdom2  9485  canthwdom  9491  isfin1-3  10306  canthp1lem2  10574  ixxssxr  13308  incexc  15800  smupf  16445  hashbc0  16974  ramz2  16993  mreexexlem3d  17610  acsfn  17623  isdrs2  18270  fpwipodrs  18504  pwmndid  18905  pwmnd  18906  clsval2  23040  mretopd  23082  comppfsc  23522  alexsubALTlem2  24038  alexsubALTlem4  24040  0no  27826  bday0  27828  0lt1s  27829  bday0b  27830  rightge0  27838  madessno  27857  oldssno  27858  newssno  27859  lltr  27879  made0  27880  eupth2lems  30333  esplyfval0  33755  vieta  33771  esum0  34240  esumcst  34254  esumpcvgval  34269  prsiga  34322  pwldsys  34348  ldgenpisyslem1  34354  carsggect  34509  kur14  35451  0hf  36412  mh-infprim2bi  36782  bj-tagss  37340  bj-0int  37466  bj-mooreset  37467  bj-ismoored0  37471  topdifinfindis  37715  0totbnd  38147  heiborlem6  38190  istopclsd  43156  ntrkbimka  44489  ntrk0kbimka  44490  clsk1indlem0  44492  ntrclscls00  44517  ntrneicls11  44541  ismnushort  44752  0pwfi  45514  dvnprodlem3  46398  pwsal  46765  salexct  46784  sge0rnn0  46818  sge00  46826  psmeasure  46921  caragen0  46956  0ome  46979  isomenndlem  46980  ovn0  47016  ovnsubadd2lem  47095  smfresal  47238  sprsymrelfvlem  47972  lincval0  48913  lco0  48925  linds0  48963