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 970
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 1118 and ax9 1120. A more convenient form of this axiom
is a9e 1121,
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 952 |
. . . . 5
 |
| 3 | vy |
. . . . . 6
| |
| 4 | 3 | cv 952 |
. . . . 5
|
| 5 | 2, 4 | wceq 953 |
. . . 4
 |
| 6 | 5 | wn 2 |
. . 3
|
| 7 | 6, 1 | wal 951 |
. 2
|
| 8 | 7 | wn 2 |
1
|
| Colors of variables: wff set class |
| This axiom is referenced by: ax4 969 ax9o 1118 a9e 1121 a16g 1271 |