Theorem 0elpw 4834

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 3972	. 2 ⊢ ∅ ⊆ 𝐴
2		0ex 4790	. . 3 ⊢ ∅ ∈ V
3	2	elpw 4164	. 2 ⊢ (∅ ∈ 𝒫 𝐴 ↔ ∅ ⊆ 𝐴)
4	1, 3	mpbir 221	1 ⊢ ∅ ∈ 𝒫 𝐴

Syntax hints:   ∈ wcel 1990   ⊆ wss 3574  ∅c0 3915  𝒫 cpw 4158

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-nul 4789

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-dif 3577  df-in 3581  df-ss 3588  df-nul 3916  df-pw 4160

This theorem is referenced by:  pwne0  4835  marypha1lem  8339  brwdom2  8478  canthwdom  8484  pwcdadom  9038  isfin1-3  9208  canthp1lem2  9475  ixxssxr  12187  incexc  14569  smupf  15200  hashbc0  15709  ramz2  15728  mreexexlem3d  16306  acsfn  16320  isdrs2  16939  fpwipodrs  17164  clsval2  20854  mretopd  20896  comppfsc  21335  alexsubALTlem2  21852  alexsubALTlem4  21854  eupth2lems  27098  esum0  30111  esumcst  30125  esumpcvgval  30140  prsiga  30194  pwldsys  30220  ldgenpisyslem1  30226  carsggect  30380  kur14  31198  0hf  32284  bj-tagss  32968  bj-0int  33055  bj-mooreset  33056  bj-ismoored0  33061  topdifinfindis  33194  0totbnd  33572  heiborlem6  33615  istopclsd  37263  ntrkbimka  38336  ntrk0kbimka  38337  clsk1indlem0  38339  ntrclscls00  38364  ntrneicls11  38388  0pwfi  39227  dvnprodlem3  40163  pwsal  40535  salexct  40552  sge0rnn0  40585  sge00  40593  psmeasure  40688  caragen0  40720  0ome  40743  isomenndlem  40744  ovn0  40780  ovnsubadd2lem  40859  smfresal  40995  sprsymrelfvlem  41740  lincval0  42204  lco0  42216  linds0  42254