Theorem equvini 1164

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
equvini	|- (x = y -> E.z(x = z /\ z = y))

Proof of Theorem equvini

Step	Hyp	Ref	Expression
1		a9e 1121	. . . . . 6 |- E.z z = y
2		equid 1122	. . . . . . . 8 |- z = z
3	2	jctl 290	. . . . . . 7 |- (z = y -> (z = z /\ z = y))
4	3	19.22i 1036	. . . . . 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 1141	. . . . . 6 |- (A.z z = x -> A.zA.z z = x)
7		ax-8 961	. . . . . . . 8 |- (z = x -> (z = z -> x = z))
8	7	a4s 981	. . . . . . 7 |- (A.z z = x -> (z = z -> x = z))
9	8	anim1d 558	. . . . . 6 |- (A.z z = x -> ((z = z /\ z = y) -> (x = z /\ z = y)))
10	6, 9	19.22d 1058	. . . . 5 |- (A.z z = x -> (E.z(z = z /\ z = y) -> E.z(x = z /\ z = y)))
11	5, 10	mpi 44	. . . 4 |- (A.z z = x -> E.z(x = z /\ z = y))
12		a9e 1121	. . . . . 6 |- E.z z = x
13		equcomi 1124	. . . . . . . 8 |- (z = x -> x = z)
14	13, 2	jctir 293	. . . . . . 7 |- (z = x -> (x = z /\ z = z))
15	14	19.22i 1036	. . . . . 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 1141	. . . . . 6 |- (A.z z = y -> A.zA.z z = y)
18		equtrr 1128	. . . . . . . 8 |- (z = y -> (z = z -> z = y))
19	18	a4s 981	. . . . . . 7 |- (A.z z = y -> (z = z -> z = y))
20	19	anim2d 559	. . . . . 6 |- (A.z z = y -> ((x = z /\ z = z) -> (x = z /\ z = y)))
21	17, 20	19.22d 1058	. . . . 5 |- (A.z z = y -> (E.z(x = z /\ z = z) -> E.z(x = z /\ z = y)))
22	16, 21	mpi 44	. . . 4 |- (A.z z = y -> E.z(x = z /\ z = y))
23	11, 22	jaoi 341	. . 3 |- ((A.z z = x \/ A.z z = y) -> E.z(x = z /\ z = y))
24	23	a1d 12	. 2 |- ((A.z z = x \/ A.z z = y) -> (x = y -> E.z(x = z /\ z = y)))
25		ioran 306	. . 3 |- (-. (A.z z = x \/ A.z z = y) <-> (-. A.z z = x /\ -. A.z z = y))
26		hbnae 1143	. . . . 5 |- (-. A.z z = x -> A.z -. A.z z = x)
27		hbnae 1143	. . . . 5 |- (-. A.z z = y -> A.z -. A.z z = y)
28	26, 27	hban 1006	. . . 4 |- ((-. A.z z = x /\ -. A.z z = y) -> A.z(-. A.z z = x /\ -. A.z z = y))
29		ax-12 965	. . . . 5 |- (-. A.z z = x -> (-. A.z z = y -> (x = y -> A.z x = y)))
30	29	imp 350	. . . 4 |- ((-. A.z z = x /\ -. A.z z = y) -> (x = y -> A.z x = y))
31		ax-8 961	. . . . . 6 |- (x = z -> (x = y -> z = y))
32	31	anc2li 302	. . . . 5 |- (x = z -> (x = y -> (x = z /\ z = y)))
33	32	equcoms 1126	. . . 4 |- (z = x -> (x = y -> (x = z /\ z = y)))
34	28, 30, 33	a4imed 1157	. . 3 |- ((-. A.z z = x /\ -. A.z z = y) -> (x = y -> E.z(x = z /\ z = y)))
35	25, 34	sylbi 199	. 2 |- (-. (A.z z = x \/ A.z z = y) -> (x = y -> E.z(x = z /\ z = y)))
36	24, 35	pm2.61i 126	1 |- (x = y -> E.z(x = z /\ z = y))

Syntax hints:  -. wn 2   -> wi 3   \/ wo 222   /\ wa 223  A.wal 951   = wceq 953  E.wex 977

This theorem is referenced by:  sbequi 1223  equvin 1270  a12lem2 1370

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 959  ax-gen 960  ax-8 961  ax-9 962  ax-10 963  ax-12 965  ax-4 970  ax-5o 972  ax-6o 975  ax-9o 1119  ax-10o 1136

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 978

Copyright terms: Public domain