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  4565  ontr2exmid  4571  onsucsssucexmid  4573  onsucelsucexmid  4576  regexmidlemm  4578  ordsoexmid  4608  ordtri2or2exmid  4617  ontri2orexmidim  4618  opthprc  4724  acexmidlema  5925  acexmidlem2  5931  tposexg  6334  2dom  6882  map1  6889  endisj  6901  ssfiexmid  6955  domfiexmid  6957  exmidpw  6987  exmidpw2en  6991  djuex  7127  exmidomni  7226  exmidonfinlem  7283  exmidfodomrlemr  7292  exmidfodomrlemrALT  7293  exmidaclem  7302  pw1dom2  7321  pw1ne1  7323  sbthom  15829