Theorem 0ex 3909

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 3908. (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 3908	. . 3 ⊢ ∃𝑥∀𝑦 ¬ 𝑦 ∈ 𝑥
2		eq0 3264	. . . 4 ⊢ (𝑥 = ∅ ↔ ∀𝑦 ¬ 𝑦 ∈ 𝑥)
3	2	exbii 1510	. . 3 ⊢ (∃𝑥 𝑥 = ∅ ↔ ∃𝑥∀𝑦 ¬ 𝑦 ∈ 𝑥)
4	1, 3	mpbir 138	. 2 ⊢ ∃𝑥 𝑥 = ∅
5	4	issetri 2579	1 ⊢ ∅ ∈ V

Syntax hints:  ¬ wn 3  ∀wal 1255   = wceq 1257  ∃wex 1395   ∈ wcel 1407  Vcvv 2572  ∅c0 3249

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-in1 552  ax-in2 553  ax-io 638  ax-5 1350  ax-7 1351  ax-gen 1352  ax-ie1 1396  ax-ie2 1397  ax-8 1409  ax-10 1410  ax-11 1411  ax-i12 1412  ax-bndl 1413  ax-4 1414  ax-17 1433  ax-i9 1437  ax-ial 1441  ax-i5r 1442  ax-ext 2036  ax-nul 3908

This theorem depends on definitions:  df-bi 114  df-tru 1260  df-nf 1364  df-sb 1660  df-clab 2041  df-cleq 2047  df-clel 2050  df-nfc 2181  df-v 2574  df-dif 2945  df-nul 3250

This theorem is referenced by:  0elpw  3942  0nep0  3943  iin0r  3947  intv  3948  snexprc  3963  p0ex  3964  0elon  4154  onm  4163  ordtriexmidlem2  4271  ordtriexmid  4272  ordtri2orexmid  4273  ontr2exmid  4275  onsucsssucexmid  4277  onsucelsucexmidlem1  4278  onsucelsucexmid  4280  regexmidlem1  4283  reg2exmidlema  4284  ordsoexmid  4311  0elsucexmid  4314  ordpwsucexmid  4319  ordtri2or2exmid  4321  peano1  4342  finds  4348  finds2  4349  0elnn  4365  opthprc  4416  nfunv  4958  fun0  4982  acexmidlema  5528  acexmidlemb  5529  acexmidlemab  5531  ovprc  5565  1st0  5796  2nd0  5797  brtpos0  5895  reldmtpos  5896  tfr0  5965  rdg0  6002  frec0g  6011  1n0  6044  el1o  6048  fnom  6058  omexg  6059  om0  6066  nnsucsssuc  6099  en0  6303  ensn1  6304  en1  6307  2dom  6313  xp1en  6325  endisj  6326  php5dom  6353  ssfiexmid  6364  diffitest  6372  ac6sfi  6380  indpi  6468  frecfzennn  9332  bj-d0clsepcl  10379  bj-indint  10385  bj-bdfindis  10402  bj-inf2vnlem1  10425