Theorem a9e 1112

Description: At least one individual exists. This is not a theorem of free logic, which is sound in empty domains; for such a logic, we would add this theorem as an axiom of set theory (Axiom 0 of [Kunen] p. 10).

Axiom ax-9 1102 is not the only axiom that is not valid in free logic; ax-4 951 is also not valid. An open problem is whether any other of our axioms are not valid in free logics.

Assertion

Ref	Expression
a9e	⊢ ∃x x = y

Proof of Theorem a9e

Step	Hyp	Ref	Expression
1		ax9a 1111	. 2 ⊢ ¬ ∀x ¬ x = y
2		df-ex 957	. 2 ⊢ (∃x x = y ↔ ¬ ∀x ¬ x = y)
3	1, 2	mpbir 190	1 ⊢ ∃x x = y

Syntax hints:  ¬ wn 2  ∀wal 950  ∃wex 956   = wceq 1099

This theorem is referenced by:  equvini 1151  ax11v2 1199  equid1 1253  ax11eq 1340  ax11el 1341  ax11inda 1348  a12stdy1 1349  zfext2 1438  sbcbrg 2630  axsep 2670  axsep2 2672  dtrucor2 2742  opabsb 2777  dmi 3283  csbima12g 3364  csbfv12g 3681  csboprg 3925  1st2val 4033  2nd2val 4034  ecelqsi 4230  axextnd 4866  csbnegg 5287

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-4 951  ax-5 952  ax-6 953  ax-gen 955  ax-9 1102

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 957

Copyright terms: Public domain