Theorem equvini 1987

Description: A variable introduction law for equality. Lemma 15 of [Monk2] p. 109, however we do not require z to be distinct from x and y (making the proof longer). (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.)

Assertion

Ref	Expression
equvini	|- (x = y -> E.z(x = z /\ z = y))

Proof of Theorem equvini

Step	Hyp	Ref	Expression
1		equcomi 1679	. . . . . 6 |- (z = x -> x = z)
2	1	alimi 1559	. . . . 5 |- (A.z z = x -> A.z x = z)
3		a9e 1951	. . . . 5 |- E.z z = y
4	2, 3	jctir 524	. . . 4 |- (A.z z = x -> (A.z x = z /\ E.z z = y))
5	4	a1d 22	. . 3 |- (A.z z = x -> (x = y -> (A.z x = z /\ E.z z = y)))
6		19.29 1596	. . 3 |- ((A.z x = z /\ E.z z = y) -> E.z(x = z /\ z = y))
7	5, 6	syl6 29	. 2 |- (A.z z = x -> (x = y -> E.z(x = z /\ z = y)))
8		a9e 1951	. . . . . 6 |- E.z z = x
9	1	eximi 1576	. . . . . 6 |- (E.z z = x -> E.z x = z)
10	8, 9	ax-mp 5	. . . . 5 |- E.z x = z
11	10	2a1i 24	. . . 4 |- (A.z z = y -> (x = y -> E.z x = z))
12	11	anc2ri 541	. . 3 |- (A.z z = y -> (x = y -> (E.z x = z /\ A.z z = y)))
13		19.29r 1597	. . 3 |- ((E.z x = z /\ A.z z = y) -> E.z(x = z /\ z = y))
14	12, 13	syl6 29	. 2 |- (A.z z = y -> (x = y -> E.z(x = z /\ z = y)))
15		ioran 476	. . 3 |- (-. (A.z z = x \/ A.z z = y) <-> (-. A.z z = x /\ -. A.z z = y))
16		nfeqf 1958	. . . 4 |- ((-. A.z z = x /\ -. A.z z = y) -> F/z x = y)
17		ax-8 1675	. . . . . 6 |- (x = z -> (x = y -> z = y))
18	17	anc2li 540	. . . . 5 |- (x = z -> (x = y -> (x = z /\ z = y)))
19	18	equcoms 1681	. . . 4 |- (z = x -> (x = y -> (x = z /\ z = y)))
20	16, 19	spimed 1977	. . 3 |- ((-. A.z z = x /\ -. A.z z = y) -> (x = y -> E.z(x = z /\ z = y)))
21	15, 20	sylbi 187	. 2 |- (-. (A.z z = x \/ A.z z = y) -> (x = y -> E.z(x = z /\ z = y)))
22	7, 14, 21	ecase3 907	1 |- (x = y -> E.z(x = z /\ z = y))

Syntax hints:  -. wn 3   -> wi 4   \/ wo 357   /\ wa 358  A.wal 1540  E.wex 1541

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925

This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1319  df-ex 1542  df-nf 1545

This theorem is referenced by:  equvin  2001  sbequi  2059