Theorem 0elpw 5297

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 4340	. 2 ⊢ ∅ ⊆ 𝐴
2		0ex 5242	. . 3 ⊢ ∅ ∈ V
3	2	elpw 4545	. 2 ⊢ (∅ ∈ 𝒫 𝐴 ↔ ∅ ⊆ 𝐴)
4	1, 3	mpbir 231	1 ⊢ ∅ ∈ 𝒫 𝐴

Syntax hints:   ∈ wcel 2114   ⊆ wss 3889  ∅c0 4273  𝒫 cpw 4541

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708  ax-nul 5241

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-dif 3892  df-ss 3906  df-nul 4274  df-pw 4543

This theorem is referenced by:  pwne0  5298  marypha1lem  9346  brwdom2  9488  canthwdom  9494  isfin1-3  10308  canthp1lem2  10576  ixxssxr  13310  incexc  15802  smupf  16447  hashbc0  16976  ramz2  16995  mreexexlem3d  17612  acsfn  17625  isdrs2  18272  fpwipodrs  18506  pwmndid  18907  pwmnd  18908  clsval2  23015  mretopd  23057  comppfsc  23497  alexsubALTlem2  24013  alexsubALTlem4  24015  0no  27801  bday0  27803  0lt1s  27804  bday0b  27805  rightge0  27813  madessno  27832  oldssno  27833  newssno  27834  lltr  27854  made0  27855  eupth2lems  30308  esplyfval0  33708  vieta  33724  esum0  34193  esumcst  34207  esumpcvgval  34222  prsiga  34275  pwldsys  34301  ldgenpisyslem1  34307  carsggect  34462  kur14  35398  0hf  36359  mh-infprim2bi  36729  bj-tagss  37287  bj-0int  37413  bj-mooreset  37414  bj-ismoored0  37418  topdifinfindis  37662  0totbnd  38094  heiborlem6  38137  istopclsd  43132  ntrkbimka  44465  ntrk0kbimka  44466  clsk1indlem0  44468  ntrclscls00  44493  ntrneicls11  44517  ismnushort  44728  0pwfi  45490  dvnprodlem3  46376  pwsal  46743  salexct  46762  sge0rnn0  46796  sge00  46804  psmeasure  46899  caragen0  46934  0ome  46957  isomenndlem  46958  ovn0  46994  ovnsubadd2lem  47073  smfresal  47216  sprsymrelfvlem  47950  lincval0  48891  lco0  48903  linds0  48941