Theorem dvelimfv 1935

Description: Like dvelimf 1939 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 1657	. . . 4 ⊢ Ⅎ𝑧 ¬ ∀𝑥 𝑥 = 𝑦
2		ax-i12 1443	. . . . . . . . 9 ⊢ (∀𝑥 𝑥 = 𝑧 ∨ (∀𝑥 𝑥 = 𝑦 ∨ ∀𝑥(𝑧 = 𝑦 → ∀𝑥 𝑧 = 𝑦)))
3		orcom 682	. . . . . . . . . 10 ⊢ ((∀𝑥 𝑥 = 𝑦 ∨ ∀𝑥(𝑧 = 𝑦 → ∀𝑥 𝑧 = 𝑦)) ↔ (∀𝑥(𝑧 = 𝑦 → ∀𝑥 𝑧 = 𝑦) ∨ ∀𝑥 𝑥 = 𝑦))
4	3	orbi2i 714	. . . . . . . . 9 ⊢ ((∀𝑥 𝑥 = 𝑧 ∨ (∀𝑥 𝑥 = 𝑦 ∨ ∀𝑥(𝑧 = 𝑦 → ∀𝑥 𝑧 = 𝑦))) ↔ (∀𝑥 𝑥 = 𝑧 ∨ (∀𝑥(𝑧 = 𝑦 → ∀𝑥 𝑧 = 𝑦) ∨ ∀𝑥 𝑥 = 𝑦)))
5	2, 4	mpbi 143	. . . . . . . 8 ⊢ (∀𝑥 𝑥 = 𝑧 ∨ (∀𝑥(𝑧 = 𝑦 → ∀𝑥 𝑧 = 𝑦) ∨ ∀𝑥 𝑥 = 𝑦))
6		orass 719	. . . . . . . 8 ⊢ (((∀𝑥 𝑥 = 𝑧 ∨ ∀𝑥(𝑧 = 𝑦 → ∀𝑥 𝑧 = 𝑦)) ∨ ∀𝑥 𝑥 = 𝑦) ↔ (∀𝑥 𝑥 = 𝑧 ∨ (∀𝑥(𝑧 = 𝑦 → ∀𝑥 𝑧 = 𝑦) ∨ ∀𝑥 𝑥 = 𝑦)))
7	5, 6	mpbir 144	. . . . . . 7 ⊢ ((∀𝑥 𝑥 = 𝑧 ∨ ∀𝑥(𝑧 = 𝑦 → ∀𝑥 𝑧 = 𝑦)) ∨ ∀𝑥 𝑥 = 𝑦)
8		nfae 1654	. . . . . . . . . . 11 ⊢ Ⅎ𝑥∀𝑥 𝑥 = 𝑧
9		ax16ALT 1787	. . . . . . . . . . 11 ⊢ (∀𝑥 𝑥 = 𝑧 → (𝑧 = 𝑦 → ∀𝑥 𝑧 = 𝑦))
10	8, 9	nfd 1461	. . . . . . . . . 10 ⊢ (∀𝑥 𝑥 = 𝑧 → Ⅎ𝑥 𝑧 = 𝑦)
11		dvelimfv.1	. . . . . . . . . . . 12 ⊢ (𝜑 → ∀𝑥𝜑)
12	11	nfi 1396	. . . . . . . . . . 11 ⊢ Ⅎ𝑥𝜑
13	12	a1i 9	. . . . . . . . . 10 ⊢ (∀𝑥 𝑥 = 𝑧 → Ⅎ𝑥𝜑)
14	10, 13	nfimd 1522	. . . . . . . . 9 ⊢ (∀𝑥 𝑥 = 𝑧 → Ⅎ𝑥(𝑧 = 𝑦 → 𝜑))
15		df-nf 1395	. . . . . . . . . 10 ⊢ (Ⅎ𝑥 𝑧 = 𝑦 ↔ ∀𝑥(𝑧 = 𝑦 → ∀𝑥 𝑧 = 𝑦))
16		id 19	. . . . . . . . . . 11 ⊢ (Ⅎ𝑥 𝑧 = 𝑦 → Ⅎ𝑥 𝑧 = 𝑦)
17	12	a1i 9	. . . . . . . . . . 11 ⊢ (Ⅎ𝑥 𝑧 = 𝑦 → Ⅎ𝑥𝜑)
18	16, 17	nfimd 1522	. . . . . . . . . 10 ⊢ (Ⅎ𝑥 𝑧 = 𝑦 → Ⅎ𝑥(𝑧 = 𝑦 → 𝜑))
19	15, 18	sylbir 133	. . . . . . . . 9 ⊢ (∀𝑥(𝑧 = 𝑦 → ∀𝑥 𝑧 = 𝑦) → Ⅎ𝑥(𝑧 = 𝑦 → 𝜑))
20	14, 19	jaoi 671	. . . . . . . 8 ⊢ ((∀𝑥 𝑥 = 𝑧 ∨ ∀𝑥(𝑧 = 𝑦 → ∀𝑥 𝑧 = 𝑦)) → Ⅎ𝑥(𝑧 = 𝑦 → 𝜑))
21	20	orim1i 712	. . . . . . 7 ⊢ (((∀𝑥 𝑥 = 𝑧 ∨ ∀𝑥(𝑧 = 𝑦 → ∀𝑥 𝑧 = 𝑦)) ∨ ∀𝑥 𝑥 = 𝑦) → (Ⅎ𝑥(𝑧 = 𝑦 → 𝜑) ∨ ∀𝑥 𝑥 = 𝑦))
22	7, 21	ax-mp 7	. . . . . 6 ⊢ (Ⅎ𝑥(𝑧 = 𝑦 → 𝜑) ∨ ∀𝑥 𝑥 = 𝑦)
23		orcom 682	. . . . . 6 ⊢ ((Ⅎ𝑥(𝑧 = 𝑦 → 𝜑) ∨ ∀𝑥 𝑥 = 𝑦) ↔ (∀𝑥 𝑥 = 𝑦 ∨ Ⅎ𝑥(𝑧 = 𝑦 → 𝜑)))
24	22, 23	mpbi 143	. . . . 5 ⊢ (∀𝑥 𝑥 = 𝑦 ∨ Ⅎ𝑥(𝑧 = 𝑦 → 𝜑))
25	24	ori 677	. . . 4 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥(𝑧 = 𝑦 → 𝜑))
26	1, 25	nfald 1690	. . 3 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥∀𝑧(𝑧 = 𝑦 → 𝜑))
27		dvelimfv.2	. . . . 5 ⊢ (𝜓 → ∀𝑧𝜓)
28		dvelimfv.3	. . . . 5 ⊢ (𝑧 = 𝑦 → (𝜑 ↔ 𝜓))
29	27, 28	equsalh 1661	. . . 4 ⊢ (∀𝑧(𝑧 = 𝑦 → 𝜑) ↔ 𝜓)
30	29	nfbii 1407	. . 3 ⊢ (Ⅎ𝑥∀𝑧(𝑧 = 𝑦 → 𝜑) ↔ Ⅎ𝑥𝜓)
31	26, 30	sylib 120	. 2 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥𝜓)
32	31	nfrd 1458	1 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝜓 → ∀𝑥𝜓))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 103   ∨ wo 664  ∀wal 1287  Ⅎwnf 1394

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in1 579  ax-in2 580  ax-io 665  ax-5 1381  ax-7 1382  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-8 1440  ax-10 1441  ax-11 1442  ax-i12 1443  ax-4 1445  ax-17 1464  ax-i9 1468  ax-ial 1472  ax-i5r 1473

This theorem depends on definitions:  df-bi 115  df-tru 1292  df-fal 1295  df-nf 1395  df-sb 1693

This theorem is referenced by: (None)