Theorem 0elpw 5316

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

This proof depends on syntax axioms:   ∈ wcel 2144   ⊆ wss 3895  ∅c0 4278  𝒫 cpw 4556

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-nul 5259

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-ss 3896  df-dif 4047  df-nul 4279  df-pw 4558

This theorem is used by:  pwne0  5317  marypha1lem  9428  brwdom2  9570  canthwdom  9576  0hf  9920  isfin1-3  10467  canthp1lem2  10741  ixxssxr  13491  incexc  16011  smupf  16653  hashbc0  17188  ramz2  17207  mreexexlem3d  17825  acsfn  17838  isdrs2  18485  fpwipodrs  18719  pwmndid  19147  pwmnd  19148  clsval2  23373  mretopd  23415  comppfsc  23856  alexsubALTlem2  24372  alexsubALTlem4  24374  0no  28200  bday0  28202  0lt1s  28203  bday0b  28204  rightge0  28212  madessno  28231  oldssno  28232  newssno  28233  lltr  28253  made0  28254  eupth2lems  30844  esplyfval0  34242  vieta  34258  esum0  34727  esumcst  34741  esumpcvgval  34756  prsiga  34809  pwldsys  34836  ldgenpisyslem1  34842  carsggect  34996  kur14  36067  mh-infprim2bi  37427  bj-tagss  37985  bj-0int  38114  bj-mooreset  38115  bj-ismoored0  38119  topdifinfindis  38362  0totbnd  38800  heiborlem6  38843  istopclsd  43804  ntrkbimka  45131  ntrk0kbimka  45132  clsk1indlem0  45134  ntrclscls00  45159  ntrneicls11  45183  ismnushort  45378  0pwfi  46169  dvnprodlem3  47051  pwsal  47418  salexct  47437  sge0rnn0  47471  sge00  47479  psmeasure  47574  caragen0  47609  0ome  47632  isomenndlem  47633  ovn0  47669  ovnsubadd2lem  47748  smfresal  47891  sprsymrelfvlem  48665  lincval0  49620  lco0  49632  linds0  49670