Axiom ax-15 1109

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 1190; see theorem ax15 1339. Alternately, ax-17 1190 becomes unnecessary in principle with this axiom, but we lose the more powerful metalogic afforded by ax-17 1190. We retain ax-15 1109 here to provide completeness for systems with the simpler metalogic that results from omitting ax-17 1190, which might be easier to study for some theoretical purposes.

Assertion

Ref	Expression
ax-15	⊢ (¬ ∀z z = x → (¬ ∀z z = y → (x ∈ y → ∀z x ∈ y)))

Detailed syntax breakdown of Axiom ax-15

Step	Hyp	Ref	Expression
1		vz	. . . . . 6 set z
2	1	cv 1098	. . . . 5 class z
3		vx	. . . . . 6 set x
4	3	cv 1098	. . . . 5 class x
5	2, 4	wceq 1099	. . . 4 wff z = x
6	5, 1	wal 950	. . 3 wff ∀z z = x
7	6	wn 2	. 2 wff ¬ ∀z z = x
8		vy	. . . . . . 7 set y
9	8	cv 1098	. . . . . 6 class y
10	2, 9	wceq 1099	. . . . 5 wff z = y
11	10, 1	wal 950	. . . 4 wff ∀z z = y
12	11	wn 2	. . 3 wff ¬ ∀z z = y
13	4, 9	wcel 1105	. . . 4 wff x ∈ y
14	13, 1	wal 950	. . . 4 wff ∀z x ∈ y
15	13, 14	wi 3	. . 3 wff (x ∈ y → ∀z x ∈ y)
16	12, 15	wi 3	. 2 wff (¬ ∀z z = y → (x ∈ y → ∀z x ∈ y))
17	7, 16	wi 3	1 wff (¬ ∀z z = x → (¬ ∀z z = y → (x ∈ y → ∀z x ∈ y)))

This axiom is referenced by:  ax17el 1196

Copyright terms: Public domain