Theorem hbequid 1313

Description: A more general version of hbequid2 1533 using ax-5 1302, ax-8 1306, ax-12 1310, and ax-gen 1305.

Assertion

Ref	Expression
hbequid	|- (x = x -> A.y x = x)

Proof of Theorem hbequid

Step	Hyp	Ref	Expression
1		ax-12 1310	. 2 |- (-. A.y y = x -> (-. A.y y = x -> (x = x -> A.y x = x)))
2		ax-8 1306	. . . . . 6 |- (y = x -> (y = x -> x = x))
3	2	pm2.43i 78	. . . . 5 |- (y = x -> x = x)
4	3	ax-gen 1305	. . . 4 |- A.y(y = x -> x = x)
5		ax-5 1302	. . . 4 |- (A.y(y = x -> x = x) -> (A.y y = x -> A.y x = x))
6	4, 5	ax-mp 7	. . 3 |- (A.y y = x -> A.y x = x)
7	6	a1d 15	. 2 |- (A.y y = x -> (x = x -> A.y x = x))
8	1, 7, 7	pm2.61ii 144	1 |- (x = x -> A.y x = x)

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

This theorem is referenced by:  equidq 1315

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-5 1302  ax-gen 1305  ax-8 1306  ax-12 1310

Copyright terms: Public domain