Theorem dvelimALT 1886

Description: Version of dvelim 1893 that doesn't use ax-10 1396. Because it has different distinct variable constraints than dvelim 1893 and is used in important proofs, it would be better if it had a name which does not end in ALT (ideally more close to set.mm naming). (Contributed by NM, 17-May-2008.) (Proof modification is discouraged.) (New usage is discouraged.)

Hypotheses

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

Assertion

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

Distinct variable groups:   𝜓,𝑧   𝑥,𝑧   𝑦,𝑧

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

Proof of Theorem dvelimALT

Step	Hyp	Ref	Expression
1		nfv 1421	. . . 4 ⊢ Ⅎ𝑧 ¬ ∀𝑥 𝑥 = 𝑦
2		ax-i12 1398	. . . . . . . . 9 ⊢ (∀𝑥 𝑥 = 𝑧 ∨ (∀𝑥 𝑥 = 𝑦 ∨ ∀𝑥(𝑧 = 𝑦 → ∀𝑥 𝑧 = 𝑦)))
3		orcom 647	. . . . . . . . . 10 ⊢ ((∀𝑥 𝑥 = 𝑦 ∨ ∀𝑥(𝑧 = 𝑦 → ∀𝑥 𝑧 = 𝑦)) ↔ (∀𝑥(𝑧 = 𝑦 → ∀𝑥 𝑧 = 𝑦) ∨ ∀𝑥 𝑥 = 𝑦))
4	3	orbi2i 679	. . . . . . . . 9 ⊢ ((∀𝑥 𝑥 = 𝑧 ∨ (∀𝑥 𝑥 = 𝑦 ∨ ∀𝑥(𝑧 = 𝑦 → ∀𝑥 𝑧 = 𝑦))) ↔ (∀𝑥 𝑥 = 𝑧 ∨ (∀𝑥(𝑧 = 𝑦 → ∀𝑥 𝑧 = 𝑦) ∨ ∀𝑥 𝑥 = 𝑦)))
5	2, 4	mpbi 133	. . . . . . . 8 ⊢ (∀𝑥 𝑥 = 𝑧 ∨ (∀𝑥(𝑧 = 𝑦 → ∀𝑥 𝑧 = 𝑦) ∨ ∀𝑥 𝑥 = 𝑦))
6		orass 684	. . . . . . . 8 ⊢ (((∀𝑥 𝑥 = 𝑧 ∨ ∀𝑥(𝑧 = 𝑦 → ∀𝑥 𝑧 = 𝑦)) ∨ ∀𝑥 𝑥 = 𝑦) ↔ (∀𝑥 𝑥 = 𝑧 ∨ (∀𝑥(𝑧 = 𝑦 → ∀𝑥 𝑧 = 𝑦) ∨ ∀𝑥 𝑥 = 𝑦)))
7	5, 6	mpbir 134	. . . . . . 7 ⊢ ((∀𝑥 𝑥 = 𝑧 ∨ ∀𝑥(𝑧 = 𝑦 → ∀𝑥 𝑧 = 𝑦)) ∨ ∀𝑥 𝑥 = 𝑦)
8		nfa1 1434	. . . . . . . . . . 11 ⊢ Ⅎ𝑥∀𝑥 𝑥 = 𝑧
9		ax16ALT 1739	. . . . . . . . . . 11 ⊢ (∀𝑥 𝑥 = 𝑧 → (𝑧 = 𝑦 → ∀𝑥 𝑧 = 𝑦))
10	8, 9	nfd 1416	. . . . . . . . . 10 ⊢ (∀𝑥 𝑥 = 𝑧 → Ⅎ𝑥 𝑧 = 𝑦)
11		dvelimALT.1	. . . . . . . . . . . 12 ⊢ (𝜑 → ∀𝑥𝜑)
12	11	nfi 1351	. . . . . . . . . . 11 ⊢ Ⅎ𝑥𝜑
13	12	a1i 9	. . . . . . . . . 10 ⊢ (∀𝑥 𝑥 = 𝑧 → Ⅎ𝑥𝜑)
14	10, 13	nfimd 1477	. . . . . . . . 9 ⊢ (∀𝑥 𝑥 = 𝑧 → Ⅎ𝑥(𝑧 = 𝑦 → 𝜑))
15		df-nf 1350	. . . . . . . . . 10 ⊢ (Ⅎ𝑥 𝑧 = 𝑦 ↔ ∀𝑥(𝑧 = 𝑦 → ∀𝑥 𝑧 = 𝑦))
16		id 19	. . . . . . . . . . 11 ⊢ (Ⅎ𝑥 𝑧 = 𝑦 → Ⅎ𝑥 𝑧 = 𝑦)
17	12	a1i 9	. . . . . . . . . . 11 ⊢ (Ⅎ𝑥 𝑧 = 𝑦 → Ⅎ𝑥𝜑)
18	16, 17	nfimd 1477	. . . . . . . . . 10 ⊢ (Ⅎ𝑥 𝑧 = 𝑦 → Ⅎ𝑥(𝑧 = 𝑦 → 𝜑))
19	15, 18	sylbir 125	. . . . . . . . 9 ⊢ (∀𝑥(𝑧 = 𝑦 → ∀𝑥 𝑧 = 𝑦) → Ⅎ𝑥(𝑧 = 𝑦 → 𝜑))
20	14, 19	jaoi 636	. . . . . . . 8 ⊢ ((∀𝑥 𝑥 = 𝑧 ∨ ∀𝑥(𝑧 = 𝑦 → ∀𝑥 𝑧 = 𝑦)) → Ⅎ𝑥(𝑧 = 𝑦 → 𝜑))
21	20	orim1i 677	. . . . . . 7 ⊢ (((∀𝑥 𝑥 = 𝑧 ∨ ∀𝑥(𝑧 = 𝑦 → ∀𝑥 𝑧 = 𝑦)) ∨ ∀𝑥 𝑥 = 𝑦) → (Ⅎ𝑥(𝑧 = 𝑦 → 𝜑) ∨ ∀𝑥 𝑥 = 𝑦))
22	7, 21	ax-mp 7	. . . . . 6 ⊢ (Ⅎ𝑥(𝑧 = 𝑦 → 𝜑) ∨ ∀𝑥 𝑥 = 𝑦)
23		orcom 647	. . . . . 6 ⊢ ((Ⅎ𝑥(𝑧 = 𝑦 → 𝜑) ∨ ∀𝑥 𝑥 = 𝑦) ↔ (∀𝑥 𝑥 = 𝑦 ∨ Ⅎ𝑥(𝑧 = 𝑦 → 𝜑)))
24	22, 23	mpbi 133	. . . . 5 ⊢ (∀𝑥 𝑥 = 𝑦 ∨ Ⅎ𝑥(𝑧 = 𝑦 → 𝜑))
25	24	ori 642	. . . 4 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥(𝑧 = 𝑦 → 𝜑))
26	1, 25	nfald 1643	. . 3 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥∀𝑧(𝑧 = 𝑦 → 𝜑))
27		ax-17 1419	. . . . 5 ⊢ (𝜓 → ∀𝑧𝜓)
28		dvelimALT.2	. . . . 5 ⊢ (𝑧 = 𝑦 → (𝜑 ↔ 𝜓))
29	27, 28	equsalh 1614	. . . 4 ⊢ (∀𝑧(𝑧 = 𝑦 → 𝜑) ↔ 𝜓)
30	29	nfbii 1362	. . 3 ⊢ (Ⅎ𝑥∀𝑧(𝑧 = 𝑦 → 𝜑) ↔ Ⅎ𝑥𝜓)
31	26, 30	sylib 127	. 2 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → Ⅎ𝑥𝜓)
32	31	nfrd 1413	1 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → (𝜓 → ∀𝑥𝜓))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 98   ∨ wo 629  ∀wal 1241  Ⅎwnf 1349

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-in2 545  ax-io 630  ax-5 1336  ax-7 1337  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-8 1395  ax-11 1397  ax-i12 1398  ax-4 1400  ax-17 1419  ax-i9 1423  ax-ial 1427  ax-i5r 1428

This theorem depends on definitions:  df-bi 110  df-nf 1350  df-sb 1646

This theorem is referenced by:  hbsb4  1888