Axiom ax-12 1627

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 2044, 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 2062.

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 1614	. . . . 5 class z
3		vx	. . . . . 6 set x
4	3	cv 1614	. . . . 5 class x
5	2, 4	wceq 1615	. . . 4 wff z = x
6	5, 1	wal 1613	. . 3 wff A.z z = x
7	6	wn 2	. 2 wff -. A.z z = x
8		vy	. . . . . . 7 set y
9	8	cv 1614	. . . . . 6 class y
10	2, 9	wceq 1615	. . . . 5 wff z = y
11	10, 1	wal 1613	. . . 4 wff A.z z = y
12	11	wn 2	. . 3 wff -. A.z z = y
13	4, 9	wceq 1615	. . . 4 wff x = y
14	13, 1	wal 1613	. . . 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 1630  equid 1795  equidALT 1796  hbae 1815  dvelimfALT 1823  equvini 1840  equveli 1841  hbequid2 1842  ax17eq 1884  hbsb4 1924  sbcom 1934  sbal1 2030  dvelimALT 2037  ax11eq 2047  ax11indalem 2052  a12stdy4 2059  a12lem1 2060  axrepndlem2 6540  axacndlem4 6557  axacnd 6559  axext4dist 14755

Copyright terms: Public domain