Theorem equidALT 1163

Description: Identity law for equality (reflexivity). Lemma 6 of [Tarski] p. 68. Alternate proof of equid 1162 directly from equality axioms ax-9 1001 and ax-12 1004.

Assertion

Ref	Expression
equidALT	|- x = x

Proof of Theorem equidALT

Step	Hyp	Ref	Expression
1		ax-9 1001	. . 3 |- -. A.x -. x = x
2		hbn1 1051	. . . 4 |- (-. A.x x = x -> A.x -. A.x x = x)
3		ax-12 1004	. . . . . . 7 |- (-. A.x x = x -> (-. A.x x = x -> (x = x -> A.x x = x)))
4	3	pm2.43i 64	. . . . . 6 |- (-. A.x x = x -> (x = x -> A.x x = x))
5	4	con3d 95	. . . . 5 |- (-. A.x x = x -> (-. A.x x = x -> -. x = x))
6	5	pm2.43i 64	. . . 4 |- (-. A.x x = x -> -. x = x)
7	2, 6	19.21ai 1034	. . 3 |- (-. A.x x = x -> A.x -. x = x)
8	1, 7	mt3 111	. 2 |- A.x x = x
9	8	a4i 1018	1 |- x = x

Syntax hints:  -. wn 2   -> wi 3  A.wal 990   = wceq 992

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 999  ax-9 1001  ax-12 1004  ax-4 1009  ax-5o 1011  ax-6o 1014

Copyright terms: Public domain