Theorem dvelimv 1939

Description: Similar to dvelim 2016 with first hypothesis replaced by distinct variable condition. (Contributed by NM, 25-Jul-2015.)

Hypothesis

Ref	Expression
dvelimv.1	⊢ (z = y → (φ ↔ ψ))

Assertion

Ref	Expression
dvelimv	⊢ (¬ ∀x x = y → (ψ → ∀xψ))

Distinct variable groups:   x,z   y,z   ψ,z   φ,x

Allowed substitution hints:   φ(y,z)   ψ(x,y)

Proof of Theorem dvelimv

Step	Hyp	Ref	Expression
1		ax-17 1616	. . . . . 6 ⊢ (ψ → ∀zψ)
2	1	a1d 22	. . . . . 6 ⊢ (ψ → (z = y → ∀zψ))
3	1, 2	alrimih 1565	. . . . 5 ⊢ (ψ → ∀z(z = y → ∀zψ))
4		sp 1747	. . . . . . . 8 ⊢ (∀zψ → ψ)
5		dvelimv.1	. . . . . . . 8 ⊢ (z = y → (φ ↔ ψ))
6	4, 5	syl5ibr 212	. . . . . . 7 ⊢ (z = y → (∀zψ → φ))
7	6	a2i 12	. . . . . 6 ⊢ ((z = y → ∀zψ) → (z = y → φ))
8	7	alimi 1559	. . . . 5 ⊢ (∀z(z = y → ∀zψ) → ∀z(z = y → φ))
9	3, 8	syl 15	. . . 4 ⊢ (ψ → ∀z(z = y → φ))
10		ax10lem3 1938	. . . . . . . 8 ⊢ (∀z z = x → ∀x x = z)
11	10	con3i 127	. . . . . . 7 ⊢ (¬ ∀x x = z → ¬ ∀z z = x)
12		hbn1 1730	. . . . . . . 8 ⊢ (¬ ∀z z = x → ∀z ¬ ∀z z = x)
13		ax10lem3 1938	. . . . . . . . 9 ⊢ (∀x x = z → ∀z z = x)
14	13	con3i 127	. . . . . . . 8 ⊢ (¬ ∀z z = x → ¬ ∀x x = z)
15	12, 14	alrimih 1565	. . . . . . 7 ⊢ (¬ ∀z z = x → ∀z ¬ ∀x x = z)
16	11, 15	syl 15	. . . . . 6 ⊢ (¬ ∀x x = z → ∀z ¬ ∀x x = z)
17		ax-17 1616	. . . . . 6 ⊢ (¬ ∀x x = y → ∀z ¬ ∀x x = y)
18	16, 17	hban 1828	. . . . 5 ⊢ ((¬ ∀x x = z ∧ ¬ ∀x x = y) → ∀z(¬ ∀x x = z ∧ ¬ ∀x x = y))
19		hbn1 1730	. . . . . . 7 ⊢ (¬ ∀x x = z → ∀x ¬ ∀x x = z)
20		hbn1 1730	. . . . . . 7 ⊢ (¬ ∀x x = y → ∀x ¬ ∀x x = y)
21	19, 20	hban 1828	. . . . . 6 ⊢ ((¬ ∀x x = z ∧ ¬ ∀x x = y) → ∀x(¬ ∀x x = z ∧ ¬ ∀x x = y))
22		ax12o 1934	. . . . . . 7 ⊢ (¬ ∀x x = z → (¬ ∀x x = y → (z = y → ∀x z = y)))
23	22	imp 418	. . . . . 6 ⊢ ((¬ ∀x x = z ∧ ¬ ∀x x = y) → (z = y → ∀x z = y))
24		a17d 1617	. . . . . 6 ⊢ ((¬ ∀x x = z ∧ ¬ ∀x x = y) → (φ → ∀xφ))
25	21, 23, 24	hbimd 1815	. . . . 5 ⊢ ((¬ ∀x x = z ∧ ¬ ∀x x = y) → ((z = y → φ) → ∀x(z = y → φ)))
26	18, 25	hbald 1740	. . . 4 ⊢ ((¬ ∀x x = z ∧ ¬ ∀x x = y) → (∀z(z = y → φ) → ∀x∀z(z = y → φ)))
27	5	biimpd 198	. . . . . . . . 9 ⊢ (z = y → (φ → ψ))
28	27	a2i 12	. . . . . . . 8 ⊢ ((z = y → φ) → (z = y → ψ))
29	28	alimi 1559	. . . . . . 7 ⊢ (∀z(z = y → φ) → ∀z(z = y → ψ))
30		ax9v 1655	. . . . . . . 8 ⊢ ¬ ∀z ¬ z = y
31		con3 126	. . . . . . . . 9 ⊢ ((z = y → ψ) → (¬ ψ → ¬ z = y))
32	31	al2imi 1561	. . . . . . . 8 ⊢ (∀z(z = y → ψ) → (∀z ¬ ψ → ∀z ¬ z = y))
33	30, 32	mtoi 169	. . . . . . 7 ⊢ (∀z(z = y → ψ) → ¬ ∀z ¬ ψ)
34	29, 33	syl 15	. . . . . 6 ⊢ (∀z(z = y → φ) → ¬ ∀z ¬ ψ)
35		ax-17 1616	. . . . . 6 ⊢ (¬ ψ → ∀z ¬ ψ)
36	34, 35	nsyl2 119	. . . . 5 ⊢ (∀z(z = y → φ) → ψ)
37	36	alimi 1559	. . . 4 ⊢ (∀x∀z(z = y → φ) → ∀xψ)
38	9, 26, 37	syl56 30	. . 3 ⊢ ((¬ ∀x x = z ∧ ¬ ∀x x = y) → (ψ → ∀xψ))
39	38	expcom 424	. 2 ⊢ (¬ ∀x x = y → (¬ ∀x x = z → (ψ → ∀xψ)))
40		sp 1747	. . . 4 ⊢ (∀x x = z → x = z)
41		ax-11 1746	. . . 4 ⊢ (x = z → (∀zψ → ∀x(x = z → ψ)))
42	40, 1, 41	syl2im 34	. . 3 ⊢ (∀x x = z → (ψ → ∀x(x = z → ψ)))
43		pm2.27 35	. . . 4 ⊢ (x = z → ((x = z → ψ) → ψ))
44	43	al2imi 1561	. . 3 ⊢ (∀x x = z → (∀x(x = z → ψ) → ∀xψ))
45	42, 44	syld 40	. 2 ⊢ (∀x x = z → (ψ → ∀xψ))
46	39, 45	pm2.61d2 152	1 ⊢ (¬ ∀x x = y → (ψ → ∀xψ))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 176   ∧ wa 358  ∀wal 1540

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-an 360  df-tru 1319  df-ex 1542  df-nf 1545

This theorem is referenced by:  dveeq2  1940  ax10lem4  1941  dveeq1  2018  dveel1  2019  dveel2  2020  rgen2a  2680