Axiom ax-c14

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

This axiom is obsolete and should no longer be used. It is proved above as theorem axc14 . (Contributed by NM, 24-Jun-1993) (New usage is discouraged.)

	Ref	Expression
Assertion	ax-c14	$$⊢\neg \forall zz=x\to \left(\neg \forall zz=y\to \left(x\in y\to \forall zx\in y\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		vz	$$setvarz$$
1	0	cv	$$setvarz$$
2		vx	$$setvarx$$
3	2	cv	$$setvarx$$
4	1 3	wceq	$$wffz=x$$
5	4 0	wal	$$wff\forall zz=x$$
6	5	wn	$$wff\neg \forall zz=x$$
7		vy	$$setvary$$
8	7	cv	$$setvary$$
9	1 8	wceq	$$wffz=y$$
10	9 0	wal	$$wff\forall zz=y$$
11	10	wn	$$wff\neg \forall zz=y$$
12	3 8	wcel	$$wffx\in y$$
13	12 0	wal	$$wff\forall zx\in y$$
14	12 13	wi	$$wff\left(x\in y\to \forall zx\in y\right)$$
15	11 14	wi	$$wff\left(\neg \forall zz=y\to \left(x\in y\to \forall zx\in y\right)\right)$$
16	6 15	wi	$$wff\left(\neg \forall zz=x\to \left(\neg \forall zz=y\to \left(x\in y\to \forall zx\in y\right)\right)\right)$$