Axiom ax-12 970

Description: Axiom of Quantifier Introduction. One of the equality and substitution axioms of predicate calculus with equality. Informally, it says that whenever z is distinct from x and y, and x = y is true, then x = y quantified with z is also true. In other words, z is irrelevant to the truth of x = y. Axiom scheme C9' in [Megill] p. 448 (p. 16 of the preprint). It apparently does not otherwise appear in the literature but is easily proved from textbook predicate calculus by cases.

An open problem is whether this axiom is redundant. Note that the analogous axiom for the membership connective, ax-15 1362, has been shown to be redundant. It is also unknown whether this axiom can be replaced by a shorter formula. However, it can be derived from two slightly shorter formulas, as shown by a12study 1380.

Assertion

Ref	Expression
ax-12	|- (-. A.z z = x -> (-. A.z z = y -> (x = y -> A.z x = y)))

Detailed syntax breakdown of Axiom ax-12

Step	Hyp	Ref	Expression
1		vz	. . . . . 6 set z
2	1	cv 957	. . . . 5 class z
3		vx	. . . . . 6 set x
4	3	cv 957	. . . . 5 class x
5	2, 4	wceq 958	. . . 4 wff z = x
6	5, 1	wal 956	. . 3 wff A.z z = x
7	6	wn 2	. 2 wff -. A.z z = x
8		vy	. . . . . . 7 set y
9	8	cv 957	. . . . . 6 class y
10	2, 9	wceq 958	. . . . 5 wff z = y
11	10, 1	wal 956	. . . 4 wff A.z z = y
12	11	wn 2	. . 3 wff -. A.z z = y
13	4, 9	wceq 958	. . . 4 wff x = y
14	13, 1	wal 956	. . . 4 wff A.z x = y
15	13, 14	wi 3	. . 3 wff (x = y -> A.z x = y)
16	12, 15	wi 3	. 2 wff (-. A.z z = y -> (x = y -> A.z x = y))
17	7, 16	wi 3	1 wff (-. A.z z = x -> (-. A.z z = y -> (x = y -> A.z x = y)))

This axiom is referenced by:  equid 1128  hbae 1147  dvelimfALT 1155  equvini 1170  hbequid 1171  ax17eq 1213  hbsb4 1250  sbcom 1260  sbal1 1348  dvelimALT 1355  ax11eq 1365  ax11indalem 1370  a12stdy4 1377  a12lem1 1378  axrepndlem2 4964  axacndlem4 4981  axacnd 4983

Copyright terms: Public domain