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 → ∃z(x = z ∧ z = y))

Proof of Theorem eqvin.l1

Step	Hyp	Ref	Expression
1		a9e 809	. . . . . 6 ⊢ ∃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 ⊢ (∃z z = y → ∃z(z = z ∧ z = y))
5	1, 4	ax-mp 6	. . . . 5 ⊢ ∃z(z = z ∧ z = y)
6		ax-8 798	. . . . . . . 8 ⊢ (z = x → (z = z → x = z))
7	6	a4s 682	. . . . . . 7 ⊢ (∀z z = x → (z = z → x = z))
8	7	anim1d 432	. . . . . 6 ⊢ (∀z z = x → ((z = z ∧ z = y) → (x = z ∧ z = y)))
9	8	del42 841	. . . . 5 ⊢ (∀z z = x → (∃z(z = z ∧ z = y) → ∃z(x = z ∧ z = y)))
10	5, 9	mpi 44	. . . 4 ⊢ (∀z z = x → ∃z(x = z ∧ z = y))
11		a9e 809	. . . . . 6 ⊢ ∃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 ⊢ (∃z z = x → ∃z(x = z ∧ z = z))
15	11, 14	ax-mp 6	. . . . 5 ⊢ ∃z(x = z ∧ z = z)
16		ax-1 3	. . . . . . . 8 ⊢ (z = y → (z = z → z = y))
17	16	a4s 682	. . . . . . 7 ⊢ (∀z z = y → (z = z → z = y))
18	17	anim2d 433	. . . . . 6 ⊢ (∀z z = y → ((x = z ∧ z = z) → (x = z ∧ z = y)))
19	18	del42 841	. . . . 5 ⊢ (∀z z = y → (∃z(x = z ∧ z = z) → ∃z(x = z ∧ z = y)))
20	15, 19	mpi 44	. . . 4 ⊢ (∀z z = y → ∃z(x = z ∧ z = y))
21	10, 20	jaoi 275	. . 3 ⊢ ((∀z z = x ∨ ∀z z = y) → ∃z(x = z ∧ z = y))
22	21	a1d 14	. 2 ⊢ ((∀z z = x ∨ ∀z z = y) → (x = y → ∃z(x = z ∧ z = y)))
23		ioran 254	. . 3 ⊢ (¬ (∀z z = x ∨ ∀z z = y) ↔ (¬ ∀z z = x ∧ ¬ ∀z z = y))
24		eq6 826	. . . . 5 ⊢ (¬ ∀z z = x → ∀z ¬ ∀z z = x)
25		eq6 826	. . . . 5 ⊢ (¬ ∀z z = y → ∀z ¬ ∀z z = y)
26	24, 25	hban 704	. . . 4 ⊢ ((¬ ∀z z = x ∧ ¬ ∀z z = y) → ∀z(¬ ∀z z = x ∧ ¬ ∀z z = y))
27		ax-12 802	. . . . 5 ⊢ (¬ ∀z z = x → (¬ ∀z z = y → (x = y → ∀z x = y)))
28	27	imp 277	. . . 4 ⊢ ((¬ ∀z z = x ∧ ¬ ∀z z = y) → (x = y → ∀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 ⊢ ((¬ ∀z z = x ∧ ¬ ∀z z = y) → (x = y → ∃z(x = z ∧ z = y)))
33	23, 32	sylbi 174	. 2 ⊢ (¬ (∀z z = x ∨ ∀z z = y) → (x = y → ∃z(x = z ∧ z = y)))
34	22, 33	pm2.61i 110	1 ⊢ (x = y → ∃z(x = z ∧ z = y))

Syntax hints:  ¬ wn 1   → wi 2   ∨ wo 195   ∧ wa 196  ∀wal 672  ∃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