Theorem 0elpw 5140

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

Syntax hints:   ∈ wcel 2079   ⊆ wss 3854  ∅c0 4206  𝒫 cpw 4447

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1775  ax-4 1789  ax-5 1886  ax-6 1945  ax-7 1990  ax-8 2081  ax-9 2089  ax-10 2110  ax-11 2124  ax-12 2139  ax-ext 2767  ax-nul 5095

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-tru 1523  df-ex 1760  df-nf 1764  df-sb 2041  df-clab 2774  df-cleq 2786  df-clel 2861  df-nfc 2933  df-v 3434  df-dif 3857  df-in 3861  df-ss 3869  df-nul 4207  df-pw 4449

This theorem is referenced by:  pwne0  5141  marypha1lem  8733  brwdom2  8873  canthwdom  8879  isfin1-3  9643  canthp1lem2  9910  ixxssxr  12589  incexc  15013  smupf  15648  hashbc0  16158  ramz2  16177  mreexexlem3d  16734  acsfn  16747  isdrs2  17366  fpwipodrs  17591  clsval2  21330  mretopd  21372  comppfsc  21812  alexsubALTlem2  22328  alexsubALTlem4  22330  eupth2lems  27693  esum0  30881  esumcst  30895  esumpcvgval  30910  prsiga  30963  pwldsys  30989  ldgenpisyslem1  30995  carsggect  31149  kur14  32027  0hf  33192  bj-tagss  33843  bj-0int  33938  bj-mooreset  33939  bj-ismoored0  33944  topdifinfindis  34104  0totbnd  34529  heiborlem6  34572  istopclsd  38732  ntrkbimka  39824  ntrk0kbimka  39825  clsk1indlem0  39827  ntrclscls00  39852  ntrneicls11  39876  0pwfi  40812  dvnprodlem3  41728  pwsal  42096  salexct  42113  sge0rnn0  42146  sge00  42154  psmeasure  42249  caragen0  42284  0ome  42307  isomenndlem  42308  ovn0  42344  ovnsubadd2lem  42423  smfresal  42559  sprsymrelfvlem  43088  lincval0  43904  lco0  43916  linds0  43954