Axiom ax-15 1360

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 971; see theorem ax15 1359. Alternately, ax-17 971 becomes unnecessary in principle with this axiom, but we lose the more powerful metalogic afforded by ax-17 971. We retain ax-15 1360 here to provide completeness for systems with the simpler metalogic that results from omitting ax-17 971, 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 955	. . . . 5 class z
3		vx	. . . . . 6 set x
4	3	cv 955	. . . . 5 class x
5	2, 4	wceq 956	. . . 4 wff z = x
6	5, 1	wal 954	. . 3 wff A.z z = x
7	6	wn 2	. 2 wff -. A.z z = x
8		vy	. . . . . . 7 set y
9	8	cv 955	. . . . . 6 class y
10	2, 9	wceq 956	. . . . 5 wff z = y
11	10, 1	wal 954	. . . 4 wff A.z z = y
12	11	wn 2	. . 3 wff -. A.z z = y
13	4, 9	wcel 958	. . . 4 wff x e. y
14	13, 1	wal 954	. . . 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 1361  ax11el 1364  axrepnd 4938  axpowndlem4 4944  axregndlem2 4947  axinfndlem1 4949  axinfnd 4950  axacndlem4 4954  axacndlem5 4955  axacnd 4956

Copyright terms: Public domain