Theorem equvini 1369

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). (The proof was 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 1325	. . . . . 6 |- (z = x -> x = z)
2	1	alimi 1176	. . . . 5 |- (A.z z = x -> A.z x = z)
3		a9e 1321	. . . . 5 |- E.z z = y
4	2, 3	jctir 315	. . . 4 |- (A.z z = x -> (A.z x = z /\ E.z z = y))
5	4	a1d 15	. . 3 |- (A.z z = x -> (x = y -> (A.z x = z /\ E.z z = y)))
6		19.29 1259	. . 3 |- ((A.z x = z /\ E.z z = y) -> E.z(x = z /\ z = y))
7	5, 6	syl6 25	. 2 |- (A.z z = x -> (x = y -> E.z(x = z /\ z = y)))
8		a9e 1321	. . . . . 6 |- E.z z = x
9	1	eximi 1225	. . . . . 6 |- (E.z z = x -> E.z x = z)
10	8, 9	ax-mp 7	. . . . 5 |- E.z x = z
11	10	a1i12 9	. . . 4 |- (A.z z = y -> (x = y -> E.z x = z))
12	11	anc2ri 325	. . 3 |- (A.z z = y -> (x = y -> (E.z x = z /\ A.z z = y)))
13		19.29r 1261	. . 3 |- ((E.z x = z /\ A.z z = y) -> E.z(x = z /\ z = y))
14	12, 13	syl6 25	. 2 |- (A.z z = y -> (x = y -> E.z(x = z /\ z = y)))
15		ioran 329	. . 3 |- (-. (A.z z = x \/ A.z z = y) <-> (-. A.z z = x /\ -. A.z z = y))
16		hbnae 1345	. . . . 5 |- (-. A.z z = x -> A.z -. A.z z = x)
17		hbnae 1345	. . . . 5 |- (-. A.z z = y -> A.z -. A.z z = y)
18	16, 17	hban 1194	. . . 4 |- ((-. A.z z = x /\ -. A.z z = y) -> A.z(-. A.z z = x /\ -. A.z z = y))
19		ax-12 1148	. . . . 5 |- (-. A.z z = x -> (-. A.z z = y -> (x = y -> A.z x = y)))
20	19	imp 375	. . . 4 |- ((-. A.z z = x /\ -. A.z z = y) -> (x = y -> A.z x = y))
21		ax-8 1144	. . . . . 6 |- (x = z -> (x = y -> z = y))
22	21	anc2li 324	. . . . 5 |- (x = z -> (x = y -> (x = z /\ z = y)))
23	22	equcoms 1327	. . . 4 |- (z = x -> (x = y -> (x = z /\ z = y)))
24	18, 20, 23	a4imed 1360	. . 3 |- ((-. A.z z = x /\ -. A.z z = y) -> (x = y -> E.z(x = z /\ z = y)))
25	15, 24	sylbi 215	. 2 |- (-. (A.z z = x \/ A.z z = y) -> (x = y -> E.z(x = z /\ z = y)))
26	7, 14, 25	ecase3 822	1 |- (x = y -> E.z(x = z /\ z = y))

Syntax hints:  -. wn 2   -> wi 3   \/ wo 238   /\ wa 239  A.wal 1134   = wceq 1136  E.wex 1164

This theorem is referenced by:  sbequi 1436  equvin 1490  a12lem2 1606

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1142  ax-gen 1143  ax-8 1144  ax-9 1145  ax-10 1146  ax-12 1148  ax-4 1157  ax-5o 1159  ax-6o 1162  ax-9o 1319  ax-10o 1338

This theorem depends on definitions:  df-bi 163  df-or 240  df-an 241  df-ex 1165

Copyright terms: Public domain