Theorem equvini 1987

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). (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 25-May-2011.)

Assertion

Ref	Expression
equvini	⊢ (x = y → ∃z(x = z ∧ z = y))

Proof of Theorem equvini

Step	Hyp	Ref	Expression
1		equcomi 1679	. . . . . 6 ⊢ (z = x → x = z)
2	1	alimi 1559	. . . . 5 ⊢ (∀z z = x → ∀z x = z)
3		a9e 1951	. . . . 5 ⊢ ∃z z = y
4	2, 3	jctir 524	. . . 4 ⊢ (∀z z = x → (∀z x = z ∧ ∃z z = y))
5	4	a1d 22	. . 3 ⊢ (∀z z = x → (x = y → (∀z x = z ∧ ∃z z = y)))
6		19.29 1596	. . 3 ⊢ ((∀z x = z ∧ ∃z z = y) → ∃z(x = z ∧ z = y))
7	5, 6	syl6 29	. 2 ⊢ (∀z z = x → (x = y → ∃z(x = z ∧ z = y)))
8		a9e 1951	. . . . . 6 ⊢ ∃z z = x
9	1	eximi 1576	. . . . . 6 ⊢ (∃z z = x → ∃z x = z)
10	8, 9	ax-mp 5	. . . . 5 ⊢ ∃z x = z
11	10	2a1i 24	. . . 4 ⊢ (∀z z = y → (x = y → ∃z x = z))
12	11	anc2ri 541	. . 3 ⊢ (∀z z = y → (x = y → (∃z x = z ∧ ∀z z = y)))
13		19.29r 1597	. . 3 ⊢ ((∃z x = z ∧ ∀z z = y) → ∃z(x = z ∧ z = y))
14	12, 13	syl6 29	. 2 ⊢ (∀z z = y → (x = y → ∃z(x = z ∧ z = y)))
15		ioran 476	. . 3 ⊢ (¬ (∀z z = x ∨ ∀z z = y) ↔ (¬ ∀z z = x ∧ ¬ ∀z z = y))
16		nfeqf 1958	. . . 4 ⊢ ((¬ ∀z z = x ∧ ¬ ∀z z = y) → Ⅎz x = y)
17		ax-8 1675	. . . . . 6 ⊢ (x = z → (x = y → z = y))
18	17	anc2li 540	. . . . 5 ⊢ (x = z → (x = y → (x = z ∧ z = y)))
19	18	equcoms 1681	. . . 4 ⊢ (z = x → (x = y → (x = z ∧ z = y)))
20	16, 19	spimed 1977	. . 3 ⊢ ((¬ ∀z z = x ∧ ¬ ∀z z = y) → (x = y → ∃z(x = z ∧ z = y)))
21	15, 20	sylbi 187	. 2 ⊢ (¬ (∀z z = x ∨ ∀z z = y) → (x = y → ∃z(x = z ∧ z = y)))
22	7, 14, 21	ecase3 907	1 ⊢ (x = y → ∃z(x = z ∧ z = y))

Syntax hints:  ¬ wn 3   → wi 4   ∨ wo 357   ∧ wa 358  ∀wal 1540  ∃wex 1541

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925

This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1319  df-ex 1542  df-nf 1545

This theorem is referenced by:  equvin  2001  sbequi  2059