Theorem 0elpw 5324

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 4353	. 2 ⊢ ∅ ⊆ 𝐴
2		0ex 5268	. . 3 ⊢ ∅ ∈ V
3	2	elpw 4564	. 2 ⊢ (∅ ∈ 𝒫 𝐴 ↔ ∅ ⊆ 𝐴)
4	1, 3	mpbir 234	1 ⊢ ∅ ∈ 𝒫 𝐴

This proof depends on syntax axioms:   ∈ wcel 2145   ⊆ wss 3902  ∅c0 4282  𝒫 cpw 4560

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734  ax-nul 5267

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3455  df-dif 3905  df-ss 3919  df-nul 4283  df-pw 4562

This theorem is used by:  pwne0  5325  marypha1lem  9407  brwdom2  9549  canthwdom  9555  isfin1-3  10392  canthp1lem2  10666  ixxssxr  13414  incexc  15930  smupf  16574  hashbc0  17103  ramz2  17122  mreexexlem3d  17740  acsfn  17753  isdrs2  18400  fpwipodrs  18634  pwmndid  19061  pwmnd  19062  clsval2  23281  mretopd  23323  comppfsc  23764  alexsubALTlem2  24280  alexsubALTlem4  24282  0no  28082  bday0  28084  0lt1s  28085  bday0b  28086  rightge0  28094  madessno  28113  oldssno  28114  newssno  28115  lltr  28135  made0  28136  eupth2lems  30726  esplyfval0  34082  vieta  34098  esum0  34567  esumcst  34581  esumpcvgval  34596  prsiga  34649  pwldsys  34676  ldgenpisyslem1  34682  carsggect  34837  kur14  35803  0hf  36765  mh-infprim2bi  37174  bj-tagss  37732  bj-0int  37859  bj-mooreset  37860  bj-ismoored0  37864  topdifinfindis  38108  0totbnd  38531  heiborlem6  38574  istopclsd  43553  ntrkbimka  44886  ntrk0kbimka  44887  clsk1indlem0  44889  ntrclscls00  44914  ntrneicls11  44938  ismnushort  45133  0pwfi  45901  dvnprodlem3  46784  pwsal  47151  salexct  47170  sge0rnn0  47204  sge00  47212  psmeasure  47307  caragen0  47342  0ome  47365  isomenndlem  47366  ovn0  47402  ovnsubadd2lem  47481  smfresal  47624  sprsymrelfvlem  48398  lincval0  49353  lco0  49365  linds0  49403