Theorem p0ex 4231

Description: The power set of the empty set (the ordinal 1) is a set. (Contributed by NM, 23-Dec-1993.)

Assertion

Ref	Expression
p0ex	⊢ {∅} ∈ V

Proof of Theorem p0ex

Step	Hyp	Ref	Expression
1		pw0 3779	. 2 ⊢ 𝒫 ∅ = {∅}
2		0ex 4170	. . 3 ⊢ ∅ ∈ V
3	2	pwex 4226	. 2 ⊢ 𝒫 ∅ ∈ V
4	1, 3	eqeltrri 2278	1 ⊢ {∅} ∈ V

Syntax hints:   ∈ wcel 2175  Vcvv 2771  ∅c0 3459  𝒫 cpw 3615  {csn 3632

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 615  ax-in2 616  ax-io 710  ax-5 1469  ax-7 1470  ax-gen 1471  ax-ie1 1515  ax-ie2 1516  ax-8 1526  ax-10 1527  ax-11 1528  ax-i12 1529  ax-bndl 1531  ax-4 1532  ax-17 1548  ax-i9 1552  ax-ial 1556  ax-i5r 1557  ax-14 2178  ax-ext 2186  ax-sep 4161  ax-nul 4169  ax-pow 4217

This theorem depends on definitions:  df-bi 117  df-tru 1375  df-nf 1483  df-sb 1785  df-clab 2191  df-cleq 2197  df-clel 2200  df-nfc 2336  df-v 2773  df-dif 3167  df-in 3171  df-ss 3178  df-nul 3460  df-pw 3617  df-sn 3638

This theorem is referenced by:  pp0ex  4232  undifexmid  4236  exmidexmid  4239  exmidundif  4249  exmidundifim  4250  exmid1stab  4251  ordtriexmidlem  4566  ontr2exmid  4572  onsucsssucexmid  4574  onsucelsucexmid  4577  regexmidlemm  4579  ordsoexmid  4609  ordtri2or2exmid  4618  ontri2orexmidim  4619  opthprc  4725  acexmidlema  5934  acexmidlem2  5940  tposexg  6343  2dom  6896  map1  6903  endisj  6918  ssfiexmid  6972  domfiexmid  6974  exmidpw  7004  exmidpw2en  7008  djuex  7144  exmidomni  7243  exmidonfinlem  7300  exmidfodomrlemr  7309  exmidfodomrlemrALT  7310  exmidaclem  7319  pw1dom2  7338  pw1ne1  7340  sbthom  15898