Theorem p0ex 4183

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 3736	. 2 ⊢ 𝒫 ∅ = {∅}
2		0ex 4125	. . 3 ⊢ ∅ ∈ V
3	2	pwex 4178	. 2 ⊢ 𝒫 ∅ ∈ V
4	1, 3	eqeltrri 2249	1 ⊢ {∅} ∈ V

Syntax hints:   ∈ wcel 2146  Vcvv 2735  ∅c0 3420  𝒫 cpw 3572  {csn 3589

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 614  ax-in2 615  ax-io 709  ax-5 1445  ax-7 1446  ax-gen 1447  ax-ie1 1491  ax-ie2 1492  ax-8 1502  ax-10 1503  ax-11 1504  ax-i12 1505  ax-bndl 1507  ax-4 1508  ax-17 1524  ax-i9 1528  ax-ial 1532  ax-i5r 1533  ax-14 2149  ax-ext 2157  ax-sep 4116  ax-nul 4124  ax-pow 4169

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1459  df-sb 1761  df-clab 2162  df-cleq 2168  df-clel 2171  df-nfc 2306  df-v 2737  df-dif 3129  df-in 3133  df-ss 3140  df-nul 3421  df-pw 3574  df-sn 3595

This theorem is referenced by:  pp0ex  4184  undifexmid  4188  exmidexmid  4191  exmidundif  4201  exmidundifim  4202  ordtriexmidlem  4512  ontr2exmid  4518  onsucsssucexmid  4520  onsucelsucexmid  4523  regexmidlemm  4525  ordsoexmid  4555  ordtri2or2exmid  4564  ontri2orexmidim  4565  opthprc  4671  acexmidlema  5856  acexmidlem2  5862  tposexg  6249  2dom  6795  map1  6802  endisj  6814  ssfiexmid  6866  domfiexmid  6868  exmidpw  6898  djuex  7032  exmidomni  7130  exmidonfinlem  7182  exmidfodomrlemr  7191  exmidfodomrlemrALT  7192  exmidaclem  7197  pw1dom2  7216  pw1ne1  7218  exmid1stab  14319  sbthom  14344