Theorem 0elpw 4760

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 3924	. 2 ⊢ ∅ ⊆ 𝐴
2		0ex 4718	. . 3 ⊢ ∅ ∈ V
3	2	elpw 4114	. 2 ⊢ (∅ ∈ 𝒫 𝐴 ↔ ∅ ⊆ 𝐴)
4	1, 3	mpbir 220	1 ⊢ ∅ ∈ 𝒫 𝐴

Syntax hints:   ∈ wcel 1977   ⊆ wss 3540  ∅c0 3874  𝒫 cpw 4108

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-nul 4717

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-dif 3543  df-in 3547  df-ss 3554  df-nul 3875  df-pw 4110

This theorem is referenced by:  pwne0  4761  marypha1lem  8222  brwdom2  8361  canthwdom  8367  pwcdadom  8921  isfin1-3  9091  canthp1lem2  9354  ixxssxr  12058  incexc  14408  smupf  15038  hashbc0  15547  ramz2  15566  mreexexlem3d  16129  acsfn  16143  isdrs2  16762  fpwipodrs  16987  clsval2  20664  mretopd  20706  comppfsc  21145  alexsubALTlem2  21662  alexsubALTlem4  21664  eupath2  26507  esum0  29438  esumcst  29452  esumpcvgval  29467  prsiga  29521  pwldsys  29547  ldgenpisyslem1  29553  carsggect  29707  kur14  30452  0hf  31454  bj-tagss  32161  topdifinfindis  32370  0totbnd  32742  heiborlem6  32785  istopclsd  36281  ntrkbimka  37356  ntrk0kbimka  37357  clsk1indlem0  37359  ntrclscls00  37384  ntrneicls11  37408  0pwfi  38252  dvnprodlem3  38838  pwsal  39211  salexct  39228  sge0rnn0  39261  sge00  39269  psmeasure  39364  caragen0  39396  0ome  39419  isomenndlem  39420  ovn0  39456  ovnsubadd2lem  39535  smfresal  39673  eupth2lems  41406  lincval0  41998  lco0  42010  linds0  42048