Theorem eqvin.l1 851

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

Proof of Theorem eqvin.l1

Step	Hyp	Ref	Expression
1		a9e 809	. . . . . 6 |- E.z z = y
2		eqid 810	. . . . . . . 8 |- z = z
3	2	jctl 238	. . . . . . 7 |- (z = y -> (z = z /\ z = y))
4	3	19.22i 723	. . . . . 6 |- (E.z z = y -> E.z(z = z /\ z = y))
5	1, 4	ax-mp 6	. . . . 5 |- E.z(z = z /\ z = y)
6		ax-8 798	. . . . . . . 8 |- (z = x -> (z = z -> x = z))
7	6	a4s 682	. . . . . . 7 |- (A.z z = x -> (z = z -> x = z))
8	7	anim1d 432	. . . . . 6 |- (A.z z = x -> ((z = z /\ z = y) -> (x = z /\ z = y)))
9	8	del42 841	. . . . 5 |- (A.z z = x -> (E.z(z = z /\ z = y) -> E.z(x = z /\ z = y)))
10	5, 9	mpi 44	. . . 4 |- (A.z z = x -> E.z(x = z /\ z = y))
11		a9e 809	. . . . . 6 |- E.z z = x
12		eqcom 811	. . . . . . . 8 |- (z = x -> x = z)
13	12, 2	jctir 241	. . . . . . 7 |- (z = x -> (x = z /\ z = z))
14	13	19.22i 723	. . . . . 6 |- (E.z z = x -> E.z(x = z /\ z = z))
15	11, 14	ax-mp 6	. . . . 5 |- E.z(x = z /\ z = z)
16		ax-1 3	. . . . . . . 8 |- (z = y -> (z = z -> z = y))
17	16	a4s 682	. . . . . . 7 |- (A.z z = y -> (z = z -> z = y))
18	17	anim2d 433	. . . . . 6 |- (A.z z = y -> ((x = z /\ z = z) -> (x = z /\ z = y)))
19	18	del42 841	. . . . 5 |- (A.z z = y -> (E.z(x = z /\ z = z) -> E.z(x = z /\ z = y)))
20	15, 19	mpi 44	. . . 4 |- (A.z z = y -> E.z(x = z /\ z = y))
21	10, 20	jaoi 275	. . 3 |- ((A.z z = x \/ A.z z = y) -> E.z(x = z /\ z = y))
22	21	a1d 14	. 2 |- ((A.z z = x \/ A.z z = y) -> (x = y -> E.z(x = z /\ z = y)))
23		ioran 254	. . 3 |- (-. (A.z z = x \/ A.z z = y) <-> (-. A.z z = x /\ -. A.z z = y))
24		eq6 826	. . . . 5 |- (-. A.z z = x -> A.z -. A.z z = x)
25		eq6 826	. . . . 5 |- (-. A.z z = y -> A.z -. A.z z = y)
26	24, 25	hban 704	. . . 4 |- ((-. A.z z = x /\ -. A.z z = y) -> A.z(-. A.z z = x /\ -. A.z z = y))
27		ax-12 802	. . . . 5 |- (-. A.z z = x -> (-. A.z z = y -> (x = y -> A.z x = y)))
28	27	imp 277	. . . 4 |- ((-. A.z z = x /\ -. A.z z = y) -> (x = y -> A.z x = y))
29		ax-8 798	. . . . . 6 |- (x = z -> (x = y -> z = y))
30	29	anc2li 250	. . . . 5 |- (x = z -> (x = y -> (x = z /\ z = y)))
31	30	eqcoms 813	. . . 4 |- (z = x -> (x = y -> (x = z /\ z = y)))
32	26, 28, 31	a4c1 844	. . 3 |- ((-. A.z z = x /\ -. A.z z = y) -> (x = y -> E.z(x = z /\ z = y)))
33	23, 32	sylbi 174	. 2 |- (-. (A.z z = x \/ A.z z = y) -> (x = y -> E.z(x = z /\ z = y)))
34	22, 33	pm2.61i 110	1 |- (x = y -> E.z(x = z /\ z = y))

Syntax hints:  -. wn 1   -> wi 2   \/ wo 195   /\ wa 196  A.wal 672  E.wex 678   = weq 797

This theorem is referenced by:  sbequi 876  eqvin 932

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-12 802

This theorem depends on definitions:  df-bi 128  df-or 197  df-an 198  df-ex 679

metamath.org