Axiom ax-15 1402

Description: Axiom of Quantifier Introduction. One of the equality and substitution axioms for a non-logical predicate in our predicate calculus with equality. Axiom scheme C14' in [Megill] p. 448 (p. 16 of the preprint). It is redundant if we include ax-17 1012; see theorem ax15 1401. Alternately, ax-17 1012 becomes unnecessary in principle with this axiom, but we lose the more powerful metalogic afforded by ax-17 1012. We retain ax-15 1402 here to provide completeness for systems with the simpler metalogic that results from omitting ax-17 1012, which 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	. . . . . 6 set z
2	1	cv 996	. . . . 5 class z
3		vx	. . . . . 6 set x
4	3	cv 996	. . . . 5 class x
5	2, 4	wceq 997	. . . 4 wff z = x
6	5, 1	wal 995	. . 3 wff A.z z = x
7	6	wn 2	. 2 wff -. A.z z = x
8		vy	. . . . . . 7 set y
9	8	cv 996	. . . . . 6 class y
10	2, 9	wceq 997	. . . . 5 wff z = y
11	10, 1	wal 995	. . . 4 wff A.z z = y
12	11	wn 2	. . 3 wff -. A.z z = y
13	4, 9	wcel 999	. . . 4 wff x e. y
14	13, 1	wal 995	. . . 4 wff A.z x e. y
15	13, 14	wi 3	. . 3 wff (x e. y -> A.z x e. y)
16	12, 15	wi 3	. 2 wff (-. A.z z = y -> (x e. y -> A.z x e. y))
17	7, 16	wi 3	1 wff (-. A.z z = x -> (-. A.z z = y -> (x e. y -> A.z x e. y)))

This axiom is referenced by:  ax17el 1403  ax11el 1406  axrepnd 5011  axpowndlem4 5017  axregndlem2 5020  axinfndlem1 5022  axinfnd 5023  axacndlem4 5027  axacndlem5 5028  axacnd 5029

Copyright terms: Public domain