Theorem 0ex 3913

Description: The Null Set Axiom of ZF set theory: the empty set exists. Corollary 5.16 of [TakeutiZaring] p. 20. For the unabbreviated version, see ax-nul 3912. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 9-Jul-2011.)

Assertion

Ref	Expression
0ex	⊢ ∅ ∈ V

Proof of Theorem 0ex

Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ax-nul 3912	. . 3 ⊢ ∃𝑥∀𝑦 ¬ 𝑦 ∈ 𝑥
2		eq0 3273	. . . 4 ⊢ (𝑥 = ∅ ↔ ∀𝑦 ¬ 𝑦 ∈ 𝑥)
3	2	exbii 1537	. . 3 ⊢ (∃𝑥 𝑥 = ∅ ↔ ∃𝑥∀𝑦 ¬ 𝑦 ∈ 𝑥)
4	1, 3	mpbir 144	. 2 ⊢ ∃𝑥 𝑥 = ∅
5	4	issetri 2609	1 ⊢ ∅ ∈ V

Syntax hints:  ¬ wn 3  ∀wal 1283   = wceq 1285  ∃wex 1422   ∈ wcel 1434  Vcvv 2602  ∅c0 3258

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in1 577  ax-in2 578  ax-io 663  ax-5 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-10 1437  ax-11 1438  ax-i12 1439  ax-bndl 1440  ax-4 1441  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469  ax-ext 2064  ax-nul 3912

This theorem depends on definitions:  df-bi 115  df-tru 1288  df-nf 1391  df-sb 1687  df-clab 2069  df-cleq 2075  df-clel 2078  df-nfc 2209  df-v 2604  df-dif 2976  df-nul 3259

This theorem is referenced by:  0elpw  3946  0nep0  3947  iin0r  3951  intv  3952  snexprc  3966  p0ex  3967  0elon  4155  onm  4164  ordtriexmidlem2  4272  ordtriexmid  4273  ordtri2orexmid  4274  ontr2exmid  4276  onsucsssucexmid  4278  onsucelsucexmidlem1  4279  onsucelsucexmid  4281  regexmidlem1  4284  reg2exmidlema  4285  ordsoexmid  4313  0elsucexmid  4316  ordpwsucexmid  4321  ordtri2or2exmid  4322  peano1  4343  finds  4349  finds2  4350  0elnn  4366  opthprc  4417  nfunv  4963  fun0  4988  acexmidlema  5534  acexmidlemb  5535  acexmidlemab  5537  ovprc  5571  1st0  5802  2nd0  5803  brtpos0  5901  reldmtpos  5902  tfr0dm  5971  rdg0  6036  frec0g  6046  1n0  6080  el1o  6084  fnom  6094  omexg  6095  om0  6102  nnsucsssuc  6136  en0  6342  ensn1  6343  en1  6346  2dom  6352  xp1en  6367  endisj  6368  php5dom  6398  ssfilem  6410  ssfiexmid  6411  domfiexmid  6413  diffitest  6421  ac6sfi  6431  unfiexmid  6438  indpi  6594  frecfzennn  9508  sizeen1  9823  sizeunlem  9828  bj-d0clsepcl  10878  bj-indint  10884  bj-bdfindis  10900  bj-inf2vnlem1  10923