Theorem 0elpw 5039

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 4181	. 2 ⊢ ∅ ⊆ 𝐴
2		0ex 4997	. . 3 ⊢ ∅ ∈ V
3	2	elpw 4368	. 2 ⊢ (∅ ∈ 𝒫 𝐴 ↔ ∅ ⊆ 𝐴)
4	1, 3	mpbir 222	1 ⊢ ∅ ∈ 𝒫 𝐴

Syntax hints:   ∈ wcel 2157   ⊆ wss 3780  ∅c0 4127  𝒫 cpw 4362

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2795  ax-nul 4996

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-clab 2804  df-cleq 2810  df-clel 2813  df-nfc 2948  df-v 3404  df-dif 3783  df-in 3787  df-ss 3794  df-nul 4128  df-pw 4364

This theorem is referenced by:  pwne0  5040  marypha1lem  8588  brwdom2  8727  canthwdom  8733  pwcdadom  9333  isfin1-3  9503  canthp1lem2  9770  ixxssxr  12425  incexc  14811  smupf  15439  hashbc0  15946  ramz2  15965  mreexexlem3d  16531  acsfn  16544  isdrs2  17164  fpwipodrs  17389  clsval2  21089  mretopd  21131  comppfsc  21570  alexsubALTlem2  22086  alexsubALTlem4  22088  eupth2lems  27434  esum0  30459  esumcst  30473  esumpcvgval  30488  prsiga  30542  pwldsys  30568  ldgenpisyslem1  30574  carsggect  30728  kur14  31543  0hf  32627  bj-tagss  33297  bj-0int  33385  bj-mooreset  33386  bj-ismoored0  33391  topdifinfindis  33529  0totbnd  33902  heiborlem6  33945  istopclsd  37783  ntrkbimka  38854  ntrk0kbimka  38855  clsk1indlem0  38857  ntrclscls00  38882  ntrneicls11  38906  0pwfi  39738  dvnprodlem3  40661  pwsal  41032  salexct  41049  sge0rnn0  41082  sge00  41090  psmeasure  41185  caragen0  41220  0ome  41243  isomenndlem  41244  ovn0  41280  ovnsubadd2lem  41359  smfresal  41495  sprsymrelfvlem  42326  lincval0  42790  lco0  42802  linds0  42840