Axiom ax-12 802

Description: Axiom of Quantifier Introduction. One of the 5 equality axioms of predicate calculus. 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.

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	. . . . 5 set z
2		vx	. . . . 5 set x
3	1, 2	weq 797	. . . 4 wff z = x
4	3, 1	wal 672	. . 3 wff A.z z = x
5	4	wn 1	. 2 wff -. A.z z = x
6		vy	. . . . . 6 set y
7	1, 6	weq 797	. . . . 5 wff z = y
8	7, 1	wal 672	. . . 4 wff A.z z = y
9	8	wn 1	. . 3 wff -. A.z z = y
10	2, 6	weq 797	. . . 4 wff x = y
11	10, 1	wal 672	. . . 4 wff A.z x = y
12	10, 11	wi 2	. . 3 wff (x = y -> A.z x = y)
13	9, 12	wi 2	. 2 wff (-. A.z z = y -> (x = y -> A.z x = y))
14	5, 13	wi 2	1 wff (-. A.z z = x -> (-. A.z z = y -> (x = y -> A.z x = y)))

This axiom is referenced by:  eqid 810  eq5 824  eqvin.l1 851  hbsb4 905  ddelimf2 907  sbcom 916  ax17eq 923  sbal1 996  axrepndlem2 3739  axacndlem4 3756  axacnd 3758

metamath.org