Theorem equviniOLD 1532

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).

Assertion

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

Proof of Theorem equviniOLD

Step	Hyp	Ref	Expression
1		a9e 1483	. . . . . 6 |- E.z z = y
2		equid 1484	. . . . . . . 8 |- z = z
3	2	jctl 314	. . . . . . 7 |- (z = y -> (z = z /\ z = y))
4	3	eximi 1387	. . . . . 6 |- (E.z z = y -> E.z(z = z /\ z = y))
5	1, 4	ax-mp 7	. . . . 5 |- E.z(z = z /\ z = y)
6		hbae 1505	. . . . . 6 |- (A.z z = x -> A.zA.z z = x)
7		ax-8 1306	. . . . . . . 8 |- (z = x -> (z = z -> x = z))
8	7	a4s 1330	. . . . . . 7 |- (A.z z = x -> (z = z -> x = z))
9	8	anim1d 619	. . . . . 6 |- (A.z z = x -> ((z = z /\ z = y) -> (x = z /\ z = y)))
10	6, 9	eximd 1410	. . . . 5 |- (A.z z = x -> (E.z(z = z /\ z = y) -> E.z(x = z /\ z = y)))
11	5, 10	mpi 55	. . . 4 |- (A.z z = x -> E.z(x = z /\ z = y))
12		a9e 1483	. . . . . 6 |- E.z z = x
13		equcomi 1487	. . . . . . . 8 |- (z = x -> x = z)
14	13, 2	jctir 317	. . . . . . 7 |- (z = x -> (x = z /\ z = z))
15	14	eximi 1387	. . . . . 6 |- (E.z z = x -> E.z(x = z /\ z = z))
16	12, 15	ax-mp 7	. . . . 5 |- E.z(x = z /\ z = z)
17		hbae 1505	. . . . . 6 |- (A.z z = y -> A.zA.z z = y)
18		equtrr 1491	. . . . . . . 8 |- (z = y -> (z = z -> z = y))
19	18	a4s 1330	. . . . . . 7 |- (A.z z = y -> (z = z -> z = y))
20	19	anim2d 620	. . . . . 6 |- (A.z z = y -> ((x = z /\ z = z) -> (x = z /\ z = y)))
21	17, 20	eximd 1410	. . . . 5 |- (A.z z = y -> (E.z(x = z /\ z = z) -> E.z(x = z /\ z = y)))
22	16, 21	mpi 55	. . . 4 |- (A.z z = y -> E.z(x = z /\ z = y))
23	11, 22	jaoi 368	. . 3 |- ((A.z z = x \/ A.z z = y) -> E.z(x = z /\ z = y))
24	23	a1d 15	. 2 |- ((A.z z = x \/ A.z z = y) -> (x = y -> E.z(x = z /\ z = y)))
25		ioran 331	. . 3 |- (-. (A.z z = x \/ A.z z = y) <-> (-. A.z z = x /\ -. A.z z = y))
26		hbnae 1507	. . . . 5 |- (-. A.z z = x -> A.z -. A.z z = x)
27		hbnae 1507	. . . . 5 |- (-. A.z z = y -> A.z -. A.z z = y)
28	26, 27	hban 1356	. . . 4 |- ((-. A.z z = x /\ -. A.z z = y) -> A.z(-. A.z z = x /\ -. A.z z = y))
29		ax-12 1310	. . . . 5 |- (-. A.z z = x -> (-. A.z z = y -> (x = y -> A.z x = y)))
30	29	imp 377	. . . 4 |- ((-. A.z z = x /\ -. A.z z = y) -> (x = y -> A.z x = y))
31		ax-8 1306	. . . . . 6 |- (x = z -> (x = y -> z = y))
32	31	anc2li 326	. . . . 5 |- (x = z -> (x = y -> (x = z /\ z = y)))
33	32	equcoms 1489	. . . 4 |- (z = x -> (x = y -> (x = z /\ z = y)))
34	28, 30, 33	a4imed 1522	. . 3 |- ((-. A.z z = x /\ -. A.z z = y) -> (x = y -> E.z(x = z /\ z = y)))
35	25, 34	sylbi 216	. 2 |- (-. (A.z z = x \/ A.z z = y) -> (x = y -> E.z(x = z /\ z = y)))
36	24, 35	pm2.61i 140	1 |- (x = y -> E.z(x = z /\ z = y))

Syntax hints:  -. wn 2   -> wi 3   \/ wo 239   /\ wa 240  A.wal 1296   = wceq 1298  E.wex 1326

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-12 1310  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-ex 1327

Copyright terms: Public domain