Axiom ax-9 799

Description: Axiom of Existence. One of the 5 equality axioms of equality in predicate calculus. This axiom in effect tells us that at least one thing exists. In this form (not requiring x and y to 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 ax9 807 and ax9a 808. A more convenient form of this axiom is a9e 809.

Assertion

Ref	Expression
ax-9	|- -. A.x -. x = y

Detailed syntax breakdown of Axiom ax-9

Step	Hyp	Ref	Expression
1		vx	. . . . 5 set x
2		vy	. . . . 5 set y
3	1, 2	weq 797	. . . 4 wff x = y
4	3	wn 1	. . 3 wff -. x = y
5	4, 1	wal 672	. 2 wff A.x -. x = y
6	5	wn 1	1 wff -. A.x -. x = y

This axiom is referenced by:  ax9 807

metamath.org