Axiom ax-12 1148

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 1589, 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 1607.

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 1135	. . . . 5 class z
3		vx	. . . . . 6 set x
4	3	cv 1135	. . . . 5 class x
5	2, 4	wceq 1136	. . . 4 wff z = x
6	5, 1	wal 1134	. . 3 wff A.z z = x
7	6	wn 2	. 2 wff -. A.z z = x
8		vy	. . . . . . 7 set y
9	8	cv 1135	. . . . . 6 class y
10	2, 9	wceq 1136	. . . . 5 wff z = y
11	10, 1	wal 1134	. . . 4 wff A.z z = y
12	11	wn 2	. . 3 wff -. A.z z = y
13	4, 9	wceq 1136	. . . 4 wff x = y
14	13, 1	wal 1134	. . . 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:  hbequid 1151  equid 1322  equidALT 1323  hbae 1343  dvelimfALT 1352  equvini 1369  equviniOLD 1370  hbequid2 1371  ax17eq 1419  hbsb4 1458  sbcom 1470  sbal1 1575  dvelimALT 1582  ax11eq 1592  ax11indalem 1597  a12stdy4 1604  a12lem1 1605  axrepndlem2 5893  axacndlem4 5910  axacnd 5912  axext4dist 13657

Copyright terms: Public domain