Theorem dvelimfv 1936

Description: Like dvelimf 1940 but with a distinct variable constraint on 𝑥 and 𝑧. (Contributed by Jim Kingdon, 6-Mar-2018.)

Hypotheses

Ref	Expression
dvelimfv.1	⊢ (𝜑 → ∀𝑥𝜑)
dvelimfv.2	⊢ (𝜓 → ∀𝑧𝜓)
dvelimfv.3	⊢ (𝑧 = 𝑦 → (𝜑 ↔ 𝜓))

Assertion

Ref	Expression
dvelimfv	⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝜓 → ∀𝑥𝜓))

Distinct variable group:   𝑥,𝑧

Allowed substitution hints:   𝜑(𝑥,𝑦,𝑧)   𝜓(𝑥,𝑦,𝑧)

Proof of Theorem dvelimfv

Step	Hyp	Ref	Expression
1		nfnae 1658	. . . 4 ⊢ Ⅎ𝑧 ¬ ∀𝑥 𝑥 = 𝑦
2		ax-i12 1444	. . . . . . . . 9 ⊢ (∀𝑥 𝑥 = 𝑧 ∨ (∀𝑥 𝑥 = 𝑦 ∨ ∀𝑥(𝑧 = 𝑦 → ∀𝑥 𝑧 = 𝑦)))
3		orcom 683	. . . . . . . . . 10 ⊢ ((∀𝑥 𝑥 = 𝑦 ∨ ∀𝑥(𝑧 = 𝑦 → ∀𝑥 𝑧 = 𝑦)) ↔ (∀𝑥(𝑧 = 𝑦 → ∀𝑥 𝑧 = 𝑦) ∨ ∀𝑥 𝑥 = 𝑦))
4	3	orbi2i 715	. . . . . . . . 9 ⊢ ((∀𝑥 𝑥 = 𝑧 ∨ (∀𝑥 𝑥 = 𝑦 ∨ ∀𝑥(𝑧 = 𝑦 → ∀𝑥 𝑧 = 𝑦))) ↔ (∀𝑥 𝑥 = 𝑧 ∨ (∀𝑥(𝑧 = 𝑦 → ∀𝑥 𝑧 = 𝑦) ∨ ∀𝑥 𝑥 = 𝑦)))
5	2, 4	mpbi 144	. . . . . . . 8 ⊢ (∀𝑥 𝑥 = 𝑧 ∨ (∀𝑥(𝑧 = 𝑦 → ∀𝑥 𝑧 = 𝑦) ∨ ∀𝑥 𝑥 = 𝑦))
6		orass 720	. . . . . . . 8 ⊢ (((∀𝑥 𝑥 = 𝑧 ∨ ∀𝑥(𝑧 = 𝑦 → ∀𝑥 𝑧 = 𝑦)) ∨ ∀𝑥 𝑥 = 𝑦) ↔ (∀𝑥 𝑥 = 𝑧 ∨ (∀𝑥(𝑧 = 𝑦 → ∀𝑥 𝑧 = 𝑦) ∨ ∀𝑥 𝑥 = 𝑦)))
7	5, 6	mpbir 145	. . . . . . 7 ⊢ ((∀𝑥 𝑥 = 𝑧 ∨ ∀𝑥(𝑧 = 𝑦 → ∀𝑥 𝑧 = 𝑦)) ∨ ∀𝑥 𝑥 = 𝑦)
8		nfae 1655	. . . . . . . . . . 11 ⊢ Ⅎ𝑥∀𝑥 𝑥 = 𝑧
9		ax16ALT 1788	. . . . . . . . . . 11 ⊢ (∀𝑥 𝑥 = 𝑧 → (𝑧 = 𝑦 → ∀𝑥 𝑧 = 𝑦))
10	8, 9	nfd 1462	. . . . . . . . . 10 ⊢ (∀𝑥 𝑥 = 𝑧 → Ⅎ𝑥 𝑧 = 𝑦)
11		dvelimfv.1	. . . . . . . . . . . 12 ⊢ (𝜑 → ∀𝑥𝜑)
12	11	nfi 1397	. . . . . . . . . . 11 ⊢ Ⅎ𝑥𝜑
13	12	a1i 9	. . . . . . . . . 10 ⊢ (∀𝑥 𝑥 = 𝑧 → Ⅎ𝑥𝜑)
14	10, 13	nfimd 1523	. . . . . . . . 9 ⊢ (∀𝑥 𝑥 = 𝑧 → Ⅎ𝑥(𝑧 = 𝑦 → 𝜑))
15		df-nf 1396	. . . . . . . . . 10 ⊢ (Ⅎ𝑥 𝑧 = 𝑦 ↔ ∀𝑥(𝑧 = 𝑦 → ∀𝑥 𝑧 = 𝑦))
16		id 19	. . . . . . . . . . 11 ⊢ (Ⅎ𝑥 𝑧 = 𝑦 → Ⅎ𝑥 𝑧 = 𝑦)
17	12	a1i 9	. . . . . . . . . . 11 ⊢ (Ⅎ𝑥 𝑧 = 𝑦 → Ⅎ𝑥𝜑)
18	16, 17	nfimd 1523	. . . . . . . . . 10 ⊢ (Ⅎ𝑥 𝑧 = 𝑦 → Ⅎ𝑥(𝑧 = 𝑦 → 𝜑))
19	15, 18	sylbir 134	. . . . . . . . 9 ⊢ (∀𝑥(𝑧 = 𝑦 → ∀𝑥 𝑧 = 𝑦) → Ⅎ𝑥(𝑧 = 𝑦 → 𝜑))
20	14, 19	jaoi 672	. . . . . . . 8 ⊢ ((∀𝑥 𝑥 = 𝑧 ∨ ∀𝑥(𝑧 = 𝑦 → ∀𝑥 𝑧 = 𝑦)) → Ⅎ𝑥(𝑧 = 𝑦 → 𝜑))
21	20	orim1i 713	. . . . . . 7 ⊢ (((∀𝑥 𝑥 = 𝑧 ∨ ∀𝑥(𝑧 = 𝑦 → ∀𝑥 𝑧 = 𝑦)) ∨ ∀𝑥 𝑥 = 𝑦) → (Ⅎ𝑥(𝑧 = 𝑦 → 𝜑) ∨ ∀𝑥 𝑥 = 𝑦))
22	7, 21	ax-mp 7	. . . . . 6 ⊢ (Ⅎ𝑥(𝑧 = 𝑦 → 𝜑) ∨ ∀𝑥 𝑥 = 𝑦)
23		orcom 683	. . . . . 6 ⊢ ((Ⅎ𝑥(𝑧 = 𝑦 → 𝜑) ∨ ∀𝑥 𝑥 = 𝑦) ↔ (∀𝑥 𝑥 = 𝑦 ∨ Ⅎ𝑥(𝑧 = 𝑦 → 𝜑)))
24	22, 23	mpbi 144	. . . . 5 ⊢ (∀𝑥 𝑥 = 𝑦 ∨ Ⅎ𝑥(𝑧 = 𝑦 → 𝜑))
25	24	ori 678	. . . 4 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥(𝑧 = 𝑦 → 𝜑))
26	1, 25	nfald 1691	. . 3 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥∀𝑧(𝑧 = 𝑦 → 𝜑))
27		dvelimfv.2	. . . . 5 ⊢ (𝜓 → ∀𝑧𝜓)
28		dvelimfv.3	. . . . 5 ⊢ (𝑧 = 𝑦 → (𝜑 ↔ 𝜓))
29	27, 28	equsalh 1662	. . . 4 ⊢ (∀𝑧(𝑧 = 𝑦 → 𝜑) ↔ 𝜓)
30	29	nfbii 1408	. . 3 ⊢ (Ⅎ𝑥∀𝑧(𝑧 = 𝑦 → 𝜑) ↔ Ⅎ𝑥𝜓)
31	26, 30	sylib 121	. 2 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥𝜓)
32	31	nfrd 1459	1 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝜓 → ∀𝑥𝜓))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 104   ∨ wo 665  ∀wal 1288  Ⅎwnf 1395

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 580  ax-in2 581  ax-io 666  ax-5 1382  ax-7 1383  ax-gen 1384  ax-ie1 1428  ax-ie2 1429  ax-8 1441  ax-10 1442  ax-11 1443  ax-i12 1444  ax-4 1446  ax-17 1465  ax-i9 1469  ax-ial 1473  ax-i5r 1474

This theorem depends on definitions:  df-bi 116  df-tru 1293  df-fal 1296  df-nf 1396  df-sb 1694

This theorem is referenced by: (None)