Axiom ax-15 806

Description: Axiom of Quantifier Introduction. One of the 3 non-logical predicate axioms of our predicate calculus. Axiom scheme C14' in [Megill] p. 448 (p. 16 of the preprint). It is redundant if we include ax-17 925; see theorem ax15 1006 below. Alternately, ax-17 925 becomes unnecessary in principle with this axiom, but we lose the more powerful metalogic provided by ax-17 925. We retain ax-15 806 here to provide completeness for systems with the simpler metalogic afforded by omitting ax-17 925, that might be easier to study for some theoretical purposes.

Assertion

Ref	Expression
ax-15	|- (-. A.z z = x -> (-. A.z z = y -> (x e. y -> A.z x e. y)))

Detailed syntax breakdown of Axiom ax-15

Step	Hyp	Ref	Expression
1		vz	. . . . 5 set z
2		vx	. . . . 5 set x
3	1, 2	weq 797	. . . 4 wff z = x
4	3, 1	wal 672	. . 3 wff A.z z = x
5	4	wn 1	. 2 wff -. A.z z = x
6		vy	. . . . . 6 set y
7	1, 6	weq 797	. . . . 5 wff z = y
8	7, 1	wal 672	. . . 4 wff A.z z = y
9	8	wn 1	. . 3 wff -. A.z z = y
10	2, 6	wel 803	. . . 4 wff x e. y
11	10, 1	wal 672	. . . 4 wff A.z x e. y
12	10, 11	wi 2	. . 3 wff (x e. y -> A.z x e. y)
13	9, 12	wi 2	. 2 wff (-. A.z z = y -> (x e. y -> A.z x e. y))
14	5, 13	wi 2	1 wff (-. A.z z = x -> (-. A.z z = y -> (x e. y -> A.z x e. y)))

This axiom is referenced by:  ax17el 924

metamath.org