Theorem equvini 1167

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 1124	. . . . . 6 |- E.z z = y
2		equid 1125	. . . . . . . 8 |- z = z
3	2	jctl 290	. . . . . . 7 |- (z = y -> (z = z /\ z = y))
4	3	19.22i 1039	. . . . . 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 1144	. . . . . 6 |- (A.z z = x -> A.zA.z z = x)
7		ax-8 963	. . . . . . . 8 |- (z = x -> (z = z -> x = z))
8	7	a4s 983	. . . . . . 7 |- (A.z z = x -> (z = z -> x = z))
9	8	anim1d 559	. . . . . 6 |- (A.z z = x -> ((z = z /\ z = y) -> (x = z /\ z = y)))
10	6, 9	19.22d 1061	. . . . 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 1124	. . . . . 6 |- E.z z = x
13		equcomi 1127	. . . . . . . 8 |- (z = x -> x = z)
14	13, 2	jctir 293	. . . . . . 7 |- (z = x -> (x = z /\ z = z))
15	14	19.22i 1039	. . . . . 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 1144	. . . . . 6 |- (A.z z = y -> A.zA.z z = y)
18		equtrr 1131	. . . . . . . 8 |- (z = y -> (z = z -> z = y))
19	18	a4s 983	. . . . . . 7 |- (A.z z = y -> (z = z -> z = y))
20	19	anim2d 560	. . . . . 6 |- (A.z z = y -> ((x = z /\ z = z) -> (x = z /\ z = y)))
21	17, 20	19.22d 1061	. . . . 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 1146	. . . . 5 |- (-. A.z z = x -> A.z -. A.z z = x)
27		hbnae 1146	. . . . 5 |- (-. A.z z = y -> A.z -. A.z z = y)
28	26, 27	hban 1008	. . . 4 |- ((-. A.z z = x /\ -. A.z z = y) -> A.z(-. A.z z = x /\ -. A.z z = y))
29		ax-12 967	. . . . 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 963	. . . . . 6 |- (x = z -> (x = y -> z = y))
32	31	anc2li 302	. . . . 5 |- (x = z -> (x = y -> (x = z /\ z = y)))
33	32	equcoms 1129	. . . 4 |- (z = x -> (x = y -> (x = z /\ z = y)))
34	28, 30, 33	a4imed 1160	. . 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 953   = wceq 955  E.wex 979

This theorem is referenced by:  sbequi 1227  equvin 1274  a12lem2 1376

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 961  ax-gen 962  ax-8 963  ax-9 964  ax-10 965  ax-12 967  ax-4 972  ax-5o 974  ax-6o 977  ax-9o 1122  ax-10o 1139

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

Copyright terms: Public domain