HomeRelated theorems
Unicode version
| Home |
Metamath Proof Explorer |
< Previous
Next >
Related theorems Unicode version |
Description: Axiom of Existence. One
of the equality and substitution axioms of
predicate calculus with equality. One thing this axiom tells us is that
at least one thing exists (although ax-4 1608
and possibly others also tell
us that, i.e. they are not valid in the empty domain of a "free
logic.")
In this form (not requiring that  and 
be distinct) it was used
in an axiom system of Tarski (see Axiom B7' in footnote 1 of
[KalishMontague] p. 81.) It is
equivalent to axiom scheme C10' in
[Megill] p. 448 (p. 16 of the preprint);
the equivalence is established by
ax9o 1762 and ax9 1764. A more convenient form of this
axiom is a9e 1765, which
has additional remarks.
Raph Levien proved the independence of this axiom from the others on 12-Apr-2005. See item 16 at http://us.metamath.org/award2003.html. |
| Ref | Expression |
|---|---|
| ax-9 |
  
 |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | vx |
. . . . . 6
 | |
| 2 | 1 | cv 1585 |
. . . . 5
 |
| 3 | vy |
. . . . . 6
| |
| 4 | 3 | cv 1585 |
. . . . 5
|
| 5 | 2, 4 | wceq 1586 |
. . . 4
 |
| 6 | 5 | wn 2 |
. . 3
|
| 7 | 6, 1 | wal 1584 |
. 2
|
| 8 | 7 | wn 2 |
1
|
| Colors of variables: wff set class |
| This axiom is referenced by: equidqe 1602 ax4 1607 ax9o 1762 a9e 1765 equidALT 1767 ax4567to4 17184 |