Axiom ax-ex 326

Description: Axiom of existence. This axiom is secretly two useful axioms in one. It states that any y has an x that is equal to it. It also states that there exists something equal to itself, when y is substituted for x.

Assertion

Ref	Expression
ax-ex	⊦ ~ ∀x~ x = y

Detailed syntax breakdown of Axiom ax-ex

Step	Hyp	Ref	Expression
1		vx	. . . . . 6 var x
2	1	nvar 203	. . . . 5 nilad x
3		vy	. . . . . 6 var y
4	3	nvar 203	. . . . 5 nilad y
5	2, 4	weq 246	. . . 4 wff x = y
6	5	wneg 3	. . 3 wff ~ x = y
7	6, 1	wal 318	. 2 wff ∀x~ x = y
8	7	wneg 3	1 wff ~ ∀x~ x = y

This axiom is referenced by: (None)