Theorem equidALT 1485

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

Assertion

Ref	Expression
equidALT	|- x = x

Proof of Theorem equidALT

Step	Hyp	Ref	Expression
1		ax-9 1307	. . 3 |- -. A.x -. x = x
2		hbn1 1362	. . . 4 |- (-. A.x x = x -> A.x -. A.x x = x)
3		ax-12 1310	. . . . . . 7 |- (-. A.x x = x -> (-. A.x x = x -> (x = x -> A.x x = x)))
4	3	pm2.43i 78	. . . . . 6 |- (-. A.x x = x -> (x = x -> A.x x = x))
5	4	con3d 111	. . . . 5 |- (-. A.x x = x -> (-. A.x x = x -> -. x = x))
6	5	pm2.43i 78	. . . 4 |- (-. A.x x = x -> -. x = x)
7	2, 6	19.21ai 1345	. . 3 |- (-. A.x x = x -> A.x -. x = x)
8	1, 7	mt3 127	. 2 |- A.x x = x
9	8	a4i 1328	1 |- x = x

Syntax hints:  -. wn 2   -> wi 3  A.wal 1296   = wceq 1298

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 1305  ax-9 1307  ax-12 1310  ax-4 1319  ax-5o 1321  ax-6o 1324

Copyright terms: Public domain