Theorem dvelimfALT 1152

Description: Proof of dvelimf 1249 without using ax-11 966. See dvelimALT 1352 for a proof (of the distinct variable version dvelim 1351) that doesn't require ax-10 965.

Hypotheses

Ref	Expression
dvelimfALT.1	⊢ (φ → ∀xφ)
dvelimfALT.2	⊢ (ψ → ∀zψ)
dvelimfALT.3	⊢ (z = y → (φ ↔ ψ))

Assertion

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

Proof of Theorem dvelimfALT

Step	Hyp	Ref	Expression
1		ax-10o 1139	. . . . . 6 ⊢ (∀z z = x → (∀z∀z(z = y → φ) → ∀x∀z(z = y → φ)))
2	1	alequcoms 1142	. . . . 5 ⊢ (∀x x = z → (∀z∀z(z = y → φ) → ∀x∀z(z = y → φ)))
3		hba1 1002	. . . . 5 ⊢ (∀z(z = y → φ) → ∀z∀z(z = y → φ))
4	2, 3	syl5 21	. . . 4 ⊢ (∀x x = z → (∀z(z = y → φ) → ∀x∀z(z = y → φ)))
5	4	a1d 12	. . 3 ⊢ (∀x x = z → (¬ ∀x x = y → (∀z(z = y → φ) → ∀x∀z(z = y → φ))))
6		hbnae 1146	. . . . . 6 ⊢ (¬ ∀x x = z → ∀z ¬ ∀x x = z)
7		hbnae 1146	. . . . . 6 ⊢ (¬ ∀x x = y → ∀z ¬ ∀x x = y)
8	6, 7	hban 1008	. . . . 5 ⊢ ((¬ ∀x x = z ⋀ ¬ ∀x x = y) → ∀z(¬ ∀x x = z ⋀ ¬ ∀x x = y))
9		hbnae 1146	. . . . . . 7 ⊢ (¬ ∀x x = z → ∀x ¬ ∀x x = z)
10		hbnae 1146	. . . . . . 7 ⊢ (¬ ∀x x = y → ∀x ¬ ∀x x = y)
11	9, 10	hban 1008	. . . . . 6 ⊢ ((¬ ∀x x = z ⋀ ¬ ∀x x = y) → ∀x(¬ ∀x x = z ⋀ ¬ ∀x x = y))
12		ax-12 967	. . . . . . 7 ⊢ (¬ ∀x x = z → (¬ ∀x x = y → (z = y → ∀x z = y)))
13	12	imp 350	. . . . . 6 ⊢ ((¬ ∀x x = z ⋀ ¬ ∀x x = y) → (z = y → ∀x z = y))
14		dvelimfALT.1	. . . . . . 7 ⊢ (φ → ∀xφ)
15	14	a1i 8	. . . . . 6 ⊢ ((¬ ∀x x = z ⋀ ¬ ∀x x = y) → (φ → ∀xφ))
16	11, 13, 15	hbimd 1109	. . . . 5 ⊢ ((¬ ∀x x = z ⋀ ¬ ∀x x = y) → ((z = y → φ) → ∀x(z = y → φ)))
17	8, 16	hbald 1112	. . . 4 ⊢ ((¬ ∀x x = z ⋀ ¬ ∀x x = y) → (∀z(z = y → φ) → ∀x∀z(z = y → φ)))
18	17	ex 373	. . 3 ⊢ (¬ ∀x x = z → (¬ ∀x x = y → (∀z(z = y → φ) → ∀x∀z(z = y → φ))))
19	5, 18	pm2.61i 126	. 2 ⊢ (¬ ∀x x = y → (∀z(z = y → φ) → ∀x∀z(z = y → φ)))
20		dvelimfALT.2	. . 3 ⊢ (ψ → ∀zψ)
21		dvelimfALT.3	. . 3 ⊢ (z = y → (φ ↔ ψ))
22	20, 21	equsal 1150	. 2 ⊢ (∀z(z = y → φ) ↔ ψ)
23	22	albii 998	. 2 ⊢ (∀x∀z(z = y → φ) ↔ ∀xψ)
24	19, 22, 23	3imtr3g 551	1 ⊢ (¬ ∀x x = y → (ψ → ∀xψ))

Syntax hints:  ¬ wn 2   → wi 3   ↔ wb 146   ⋀ wa 223  ∀wal 953   = wceq 955

This theorem is referenced by:  dveeq2 1211  dveeq2ALT 1212  dveeq1 1353  dveeq1ALT 1354  dveel1 1355  dveel2 1356  ax15 1358  dveel2ALT 1361  ax11el 1363

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 961  ax-gen 962  ax-10 965  ax-12 967  ax-4 972  ax-5o 974  ax-6o 977  ax-9o 1122  ax-10o 1139

This theorem depends on definitions:  df-bi 147  df-an 225

Copyright terms: Public domain