Axiom ax-12 1104

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 1109, 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 1355.

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 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 A.z z = x
7	6	wn 2	. 2 wff -. A.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 A.z z = y
12	11	wn 2	. . 3 wff -. A.z z = y
13	4, 9	wceq 1099	. . . 4 wff x = y
14	13, 1	wal 950	. . . 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 1113  hbae 1128  dvelimfALT 1136  equvini 1151  hbequid 1152  ax17eq 1195  hbsb4 1232  sbcom 1242  sbal1 1328  ax11eq 1340  ax11indalem 1345  a12stdy4 1352  a12lem1 1353  axrepndlem2 4868  axacndlem4 4885  axacnd 4887

Copyright terms: Public domain