Theorem equidqe 1314

Description: equid 1484 with existential quantifier without using ax-4 1319 or ax-17 1317.

Assertion

Ref	Expression
equidqe	|- -. A.y -. x = x

Proof of Theorem equidqe

Step	Hyp	Ref	Expression
1		ax-9 1307	. 2 |- -. A.y -. y = x
2		ax-8 1306	. . . . . 6 |- (y = x -> (y = x -> x = x))
3	2	pm2.43i 78	. . . . 5 |- (y = x -> x = x)
4	3	con3i 114	. . . 4 |- (-. x = x -> -. y = x)
5	4	ax-gen 1305	. . 3 |- A.y(-. x = x -> -. y = x)
6		ax-5 1302	. . 3 |- (A.y(-. x = x -> -. y = x) -> (A.y -. x = x -> A.y -. y = x))
7	5, 6	ax-mp 7	. 2 |- (A.y -. x = x -> A.y -. y = x)
8	1, 7	mto 121	1 |- -. A.y -. x = x

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

This theorem is referenced by:  equidq 1315  ax4sp1 1316

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-9 1307

Copyright terms: Public domain