Axiom ax-15 1358

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 969; see theorem ax15 1357. Alternately, ax-17 969 becomes unnecessary in principle with this axiom, but we lose the more powerful metalogic afforded by ax-17 969. We retain ax-15 1358 here to provide completeness for systems with the simpler metalogic that results from omitting ax-17 969, 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 953	. . . . 5 class z
3		vx	. . . . . 6 set x
4	3	cv 953	. . . . 5 class x
5	2, 4	wceq 954	. . . 4 wff z = x
6	5, 1	wal 952	. . 3 wff A.z z = x
7	6	wn 2	. 2 wff -. A.z z = x
8		vy	. . . . . . 7 set y
9	8	cv 953	. . . . . 6 class y
10	2, 9	wceq 954	. . . . 5 wff z = y
11	10, 1	wal 952	. . . 4 wff A.z z = y
12	11	wn 2	. . 3 wff -. A.z z = y
13	4, 9	wcel 956	. . . 4 wff x e. y
14	13, 1	wal 952	. . . 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 1359  ax11el 1362  axrepnd 4926  axpowndlem4 4932  axregndlem2 4935  axinfndlem1 4937  axinfnd 4938  axacndlem4 4942  axacndlem5 4943  axacnd 4944

Copyright terms: Public domain