Theorem dvelimfv 1999

Description: Like dvelimf 2003 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 1710	. . . 4 ⊢ Ⅎ𝑧 ¬ ∀𝑥 𝑥 = 𝑦
2		ax12or 1496	. . . . . . . . 9 ⊢ (∀𝑥 𝑥 = 𝑧 ∨ (∀𝑥 𝑥 = 𝑦 ∨ ∀𝑥(𝑧 = 𝑦 → ∀𝑥 𝑧 = 𝑦)))
3		orcom 718	. . . . . . . . . 10 ⊢ ((∀𝑥 𝑥 = 𝑦 ∨ ∀𝑥(𝑧 = 𝑦 → ∀𝑥 𝑧 = 𝑦)) ↔ (∀𝑥(𝑧 = 𝑦 → ∀𝑥 𝑧 = 𝑦) ∨ ∀𝑥 𝑥 = 𝑦))
4	3	orbi2i 752	. . . . . . . . 9 ⊢ ((∀𝑥 𝑥 = 𝑧 ∨ (∀𝑥 𝑥 = 𝑦 ∨ ∀𝑥(𝑧 = 𝑦 → ∀𝑥 𝑧 = 𝑦))) ↔ (∀𝑥 𝑥 = 𝑧 ∨ (∀𝑥(𝑧 = 𝑦 → ∀𝑥 𝑧 = 𝑦) ∨ ∀𝑥 𝑥 = 𝑦)))
5	2, 4	mpbi 144	. . . . . . . 8 ⊢ (∀𝑥 𝑥 = 𝑧 ∨ (∀𝑥(𝑧 = 𝑦 → ∀𝑥 𝑧 = 𝑦) ∨ ∀𝑥 𝑥 = 𝑦))
6		orass 757	. . . . . . . 8 ⊢ (((∀𝑥 𝑥 = 𝑧 ∨ ∀𝑥(𝑧 = 𝑦 → ∀𝑥 𝑧 = 𝑦)) ∨ ∀𝑥 𝑥 = 𝑦) ↔ (∀𝑥 𝑥 = 𝑧 ∨ (∀𝑥(𝑧 = 𝑦 → ∀𝑥 𝑧 = 𝑦) ∨ ∀𝑥 𝑥 = 𝑦)))
7	5, 6	mpbir 145	. . . . . . 7 ⊢ ((∀𝑥 𝑥 = 𝑧 ∨ ∀𝑥(𝑧 = 𝑦 → ∀𝑥 𝑧 = 𝑦)) ∨ ∀𝑥 𝑥 = 𝑦)
8		nfae 1707	. . . . . . . . . . 11 ⊢ Ⅎ𝑥∀𝑥 𝑥 = 𝑧
9		ax16ALT 1847	. . . . . . . . . . 11 ⊢ (∀𝑥 𝑥 = 𝑧 → (𝑧 = 𝑦 → ∀𝑥 𝑧 = 𝑦))
10	8, 9	nfd 1511	. . . . . . . . . 10 ⊢ (∀𝑥 𝑥 = 𝑧 → Ⅎ𝑥 𝑧 = 𝑦)
11		dvelimfv.1	. . . . . . . . . . . 12 ⊢ (𝜑 → ∀𝑥𝜑)
12	11	nfi 1450	. . . . . . . . . . 11 ⊢ Ⅎ𝑥𝜑
13	12	a1i 9	. . . . . . . . . 10 ⊢ (∀𝑥 𝑥 = 𝑧 → Ⅎ𝑥𝜑)
14	10, 13	nfimd 1573	. . . . . . . . 9 ⊢ (∀𝑥 𝑥 = 𝑧 → Ⅎ𝑥(𝑧 = 𝑦 → 𝜑))
15		df-nf 1449	. . . . . . . . . 10 ⊢ (Ⅎ𝑥 𝑧 = 𝑦 ↔ ∀𝑥(𝑧 = 𝑦 → ∀𝑥 𝑧 = 𝑦))
16		id 19	. . . . . . . . . . 11 ⊢ (Ⅎ𝑥 𝑧 = 𝑦 → Ⅎ𝑥 𝑧 = 𝑦)
17	12	a1i 9	. . . . . . . . . . 11 ⊢ (Ⅎ𝑥 𝑧 = 𝑦 → Ⅎ𝑥𝜑)
18	16, 17	nfimd 1573	. . . . . . . . . 10 ⊢ (Ⅎ𝑥 𝑧 = 𝑦 → Ⅎ𝑥(𝑧 = 𝑦 → 𝜑))
19	15, 18	sylbir 134	. . . . . . . . 9 ⊢ (∀𝑥(𝑧 = 𝑦 → ∀𝑥 𝑧 = 𝑦) → Ⅎ𝑥(𝑧 = 𝑦 → 𝜑))
20	14, 19	jaoi 706	. . . . . . . 8 ⊢ ((∀𝑥 𝑥 = 𝑧 ∨ ∀𝑥(𝑧 = 𝑦 → ∀𝑥 𝑧 = 𝑦)) → Ⅎ𝑥(𝑧 = 𝑦 → 𝜑))
21	20	orim1i 750	. . . . . . 7 ⊢ (((∀𝑥 𝑥 = 𝑧 ∨ ∀𝑥(𝑧 = 𝑦 → ∀𝑥 𝑧 = 𝑦)) ∨ ∀𝑥 𝑥 = 𝑦) → (Ⅎ𝑥(𝑧 = 𝑦 → 𝜑) ∨ ∀𝑥 𝑥 = 𝑦))
22	7, 21	ax-mp 5	. . . . . 6 ⊢ (Ⅎ𝑥(𝑧 = 𝑦 → 𝜑) ∨ ∀𝑥 𝑥 = 𝑦)
23		orcom 718	. . . . . 6 ⊢ ((Ⅎ𝑥(𝑧 = 𝑦 → 𝜑) ∨ ∀𝑥 𝑥 = 𝑦) ↔ (∀𝑥 𝑥 = 𝑦 ∨ Ⅎ𝑥(𝑧 = 𝑦 → 𝜑)))
24	22, 23	mpbi 144	. . . . 5 ⊢ (∀𝑥 𝑥 = 𝑦 ∨ Ⅎ𝑥(𝑧 = 𝑦 → 𝜑))
25	24	ori 713	. . . 4 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥(𝑧 = 𝑦 → 𝜑))
26	1, 25	nfald 1748	. . 3 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥∀𝑧(𝑧 = 𝑦 → 𝜑))
27		dvelimfv.2	. . . . 5 ⊢ (𝜓 → ∀𝑧𝜓)
28		dvelimfv.3	. . . . 5 ⊢ (𝑧 = 𝑦 → (𝜑 ↔ 𝜓))
29	27, 28	equsalh 1714	. . . 4 ⊢ (∀𝑧(𝑧 = 𝑦 → 𝜑) ↔ 𝜓)
30	29	nfbii 1461	. . 3 ⊢ (Ⅎ𝑥∀𝑧(𝑧 = 𝑦 → 𝜑) ↔ Ⅎ𝑥𝜓)
31	26, 30	sylib 121	. 2 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥𝜓)
32	31	nfrd 1508	1 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝜓 → ∀𝑥𝜓))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 104   ∨ wo 698  ∀wal 1341  Ⅎwnf 1448

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 604  ax-in2 605  ax-io 699  ax-5 1435  ax-7 1436  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-8 1492  ax-10 1493  ax-11 1494  ax-i12 1495  ax-4 1498  ax-17 1514  ax-i9 1518  ax-ial 1522  ax-i5r 1523

This theorem depends on definitions:  df-bi 116  df-tru 1346  df-fal 1349  df-nf 1449  df-sb 1751

This theorem is referenced by: (None)