Theorem dvelimALT 1883

Description: Version of dvelim 1890 that doesn't use ax-10 1393. Because it has different distinct variable constraints than dvelim 1890 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	⊢ (φ → ∀xφ)
dvelimALT.2	⊢ (z = y → (φ ↔ ψ))

Assertion

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

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

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

Proof of Theorem dvelimALT

Step	Hyp	Ref	Expression
1		nfv 1418	. . . 4 ⊢ Ⅎz ¬ ∀x x = y
2		ax-i12 1395	. . . . . . . . 9 ⊢ (∀x x = z ∨ (∀x x = y ∨ ∀x(z = y → ∀x z = y)))
3		orcom 646	. . . . . . . . . 10 ⊢ ((∀x x = y ∨ ∀x(z = y → ∀x z = y)) ↔ (∀x(z = y → ∀x z = y) ∨ ∀x x = y))
4	3	orbi2i 678	. . . . . . . . 9 ⊢ ((∀x x = z ∨ (∀x x = y ∨ ∀x(z = y → ∀x z = y))) ↔ (∀x x = z ∨ (∀x(z = y → ∀x z = y) ∨ ∀x x = y)))
5	2, 4	mpbi 133	. . . . . . . 8 ⊢ (∀x x = z ∨ (∀x(z = y → ∀x z = y) ∨ ∀x x = y))
6		orass 683	. . . . . . . 8 ⊢ (((∀x x = z ∨ ∀x(z = y → ∀x z = y)) ∨ ∀x x = y) ↔ (∀x x = z ∨ (∀x(z = y → ∀x z = y) ∨ ∀x x = y)))
7	5, 6	mpbir 134	. . . . . . 7 ⊢ ((∀x x = z ∨ ∀x(z = y → ∀x z = y)) ∨ ∀x x = y)
8		nfa1 1431	. . . . . . . . . . 11 ⊢ Ⅎx∀x x = z
9		ax16ALT 1736	. . . . . . . . . . 11 ⊢ (∀x x = z → (z = y → ∀x z = y))
10	8, 9	nfd 1413	. . . . . . . . . 10 ⊢ (∀x x = z → Ⅎx z = y)
11		dvelimALT.1	. . . . . . . . . . . 12 ⊢ (φ → ∀xφ)
12	11	nfi 1348	. . . . . . . . . . 11 ⊢ Ⅎxφ
13	12	a1i 9	. . . . . . . . . 10 ⊢ (∀x x = z → Ⅎxφ)
14	10, 13	nfimd 1474	. . . . . . . . 9 ⊢ (∀x x = z → Ⅎx(z = y → φ))
15		df-nf 1347	. . . . . . . . . 10 ⊢ (Ⅎx z = y ↔ ∀x(z = y → ∀x z = y))
16		id 19	. . . . . . . . . . 11 ⊢ (Ⅎx z = y → Ⅎx z = y)
17	12	a1i 9	. . . . . . . . . . 11 ⊢ (Ⅎx z = y → Ⅎxφ)
18	16, 17	nfimd 1474	. . . . . . . . . 10 ⊢ (Ⅎx z = y → Ⅎx(z = y → φ))
19	15, 18	sylbir 125	. . . . . . . . 9 ⊢ (∀x(z = y → ∀x z = y) → Ⅎx(z = y → φ))
20	14, 19	jaoi 635	. . . . . . . 8 ⊢ ((∀x x = z ∨ ∀x(z = y → ∀x z = y)) → Ⅎx(z = y → φ))
21	20	orim1i 676	. . . . . . 7 ⊢ (((∀x x = z ∨ ∀x(z = y → ∀x z = y)) ∨ ∀x x = y) → (Ⅎx(z = y → φ) ∨ ∀x x = y))
22	7, 21	ax-mp 7	. . . . . 6 ⊢ (Ⅎx(z = y → φ) ∨ ∀x x = y)
23		orcom 646	. . . . . 6 ⊢ ((Ⅎx(z = y → φ) ∨ ∀x x = y) ↔ (∀x x = y ∨ Ⅎx(z = y → φ)))
24	22, 23	mpbi 133	. . . . 5 ⊢ (∀x x = y ∨ Ⅎx(z = y → φ))
25	24	ori 641	. . . 4 ⊢ (¬ ∀x x = y → Ⅎx(z = y → φ))
26	1, 25	nfald 1640	. . 3 ⊢ (¬ ∀x x = y → Ⅎx∀z(z = y → φ))
27		ax-17 1416	. . . . 5 ⊢ (ψ → ∀zψ)
28		dvelimALT.2	. . . . 5 ⊢ (z = y → (φ ↔ ψ))
29	27, 28	equsalh 1611	. . . 4 ⊢ (∀z(z = y → φ) ↔ ψ)
30	29	nfbii 1359	. . 3 ⊢ (Ⅎx∀z(z = y → φ) ↔ Ⅎxψ)
31	26, 30	sylib 127	. 2 ⊢ (¬ ∀x x = y → Ⅎxψ)
32	31	nfrd 1410	1 ⊢ (¬ ∀x x = y → (ψ → ∀xψ))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 98   ∨ wo 628  ∀wal 1240  Ⅎwnf 1346

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 629  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-11 1394  ax-i12 1395  ax-4 1397  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425

This theorem depends on definitions:  df-bi 110  df-nf 1347  df-sb 1643

This theorem is referenced by:  hbsb4  1885