Theorem hbsb4 1246

Description: A variable not free remains so after substitution with a distinct variable.

Hypothesis

Ref	Expression
hbsb4.1	⊢ (φ → ∀zφ)

Assertion

Ref	Expression
hbsb4	⊢ (¬ ∀z z = y → ([y / x]φ → ∀z[y / x]φ))

Proof of Theorem hbsb4

Step	Hyp	Ref	Expression
1		equequ1 1132	. . . . . 6 ⊢ (z = x → (z = y ↔ x = y))
2	1	a4s 982	. . . . 5 ⊢ (∀z z = x → (z = y ↔ x = y))
3	2	dral1 1152	. . . 4 ⊢ (∀z z = x → (∀z z = y ↔ ∀x x = y))
4	3	negbid 610	. . 3 ⊢ (∀z z = x → (¬ ∀z z = y ↔ ¬ ∀x x = y))
5		hbsb2 1225	. . . 4 ⊢ (¬ ∀x x = y → ([y / x]φ → ∀x[y / x]φ))
6		ax-10o 1138	. . . . 5 ⊢ (∀x x = z → (∀x[y / x]φ → ∀z[y / x]φ))
7	6	alequcoms 1141	. . . 4 ⊢ (∀z z = x → (∀x[y / x]φ → ∀z[y / x]φ))
8	5, 7	syl9r 58	. . 3 ⊢ (∀z z = x → (¬ ∀x x = y → ([y / x]φ → ∀z[y / x]φ)))
9	4, 8	sylbid 203	. 2 ⊢ (∀z z = x → (¬ ∀z z = y → ([y / x]φ → ∀z[y / x]φ)))
10		hbae 1143	. . . . . 6 ⊢ (∀x x = y → ∀z∀x x = y)
11		ax-4 971	. . . . . . 7 ⊢ (∀x x = y → x = y)
12	11	19.20i 990	. . . . . 6 ⊢ (∀z∀x x = y → ∀z x = y)
13		sbequ2 1177	. . . . . . . 8 ⊢ (x = y → ([y / x]φ → φ))
14	13	a4s 982	. . . . . . 7 ⊢ (∀z x = y → ([y / x]φ → φ))
15		sbequ1 1176	. . . . . . . . 9 ⊢ (x = y → (φ → [y / x]φ))
16	15	19.20ii 993	. . . . . . . 8 ⊢ (∀z x = y → (∀zφ → ∀z[y / x]φ))
17		hbsb4.1	. . . . . . . 8 ⊢ (φ → ∀zφ)
18	16, 17	syl5 21	. . . . . . 7 ⊢ (∀z x = y → (φ → ∀z[y / x]φ))
19	14, 18	syld 27	. . . . . 6 ⊢ (∀z x = y → ([y / x]φ → ∀z[y / x]φ))
20	10, 12, 19	3syl 20	. . . . 5 ⊢ (∀x x = y → ([y / x]φ → ∀z[y / x]φ))
21	20	a1d 12	. . . 4 ⊢ (∀x x = y → ((¬ ∀z z = x ⋀ ¬ ∀z z = y) → ([y / x]φ → ∀z[y / x]φ)))
22		sb4 1221	. . . . 5 ⊢ (¬ ∀x x = y → ([y / x]φ → ∀x(x = y → φ)))
23		hbnae 1145	. . . . . . . 8 ⊢ (¬ ∀z z = x → ∀x ¬ ∀z z = x)
24		hbnae 1145	. . . . . . . 8 ⊢ (¬ ∀z z = y → ∀x ¬ ∀z z = y)
25	23, 24	hban 1007	. . . . . . 7 ⊢ ((¬ ∀z z = x ⋀ ¬ ∀z z = y) → ∀x(¬ ∀z z = x ⋀ ¬ ∀z z = y))
26		hbnae 1145	. . . . . . . . 9 ⊢ (¬ ∀z z = x → ∀z ¬ ∀z z = x)
27		hbnae 1145	. . . . . . . . 9 ⊢ (¬ ∀z z = y → ∀z ¬ ∀z z = y)
28	26, 27	hban 1007	. . . . . . . 8 ⊢ ((¬ ∀z z = x ⋀ ¬ ∀z z = y) → ∀z(¬ ∀z z = x ⋀ ¬ ∀z z = y))
29		ax-12 966	. . . . . . . . 9 ⊢ (¬ ∀z z = x → (¬ ∀z z = y → (x = y → ∀z x = y)))
30	29	imp 350	. . . . . . . 8 ⊢ ((¬ ∀z z = x ⋀ ¬ ∀z z = y) → (x = y → ∀z x = y))
31	17	a1i 8	. . . . . . . 8 ⊢ ((¬ ∀z z = x ⋀ ¬ ∀z z = y) → (φ → ∀zφ))
32	28, 30, 31	hbimd 1108	. . . . . . 7 ⊢ ((¬ ∀z z = x ⋀ ¬ ∀z z = y) → ((x = y → φ) → ∀z(x = y → φ)))
33	25, 32	19.20d 994	. . . . . 6 ⊢ ((¬ ∀z z = x ⋀ ¬ ∀z z = y) → (∀x(x = y → φ) → ∀x∀z(x = y → φ)))
34		sb2 1175	. . . . . . . 8 ⊢ (∀x(x = y → φ) → [y / x]φ)
35	34	19.20i 990	. . . . . . 7 ⊢ (∀z∀x(x = y → φ) → ∀z[y / x]φ)
36	35	a7s 989	. . . . . 6 ⊢ (∀x∀z(x = y → φ) → ∀z[y / x]φ)
37	33, 36	syl6 22	. . . . 5 ⊢ ((¬ ∀z z = x ⋀ ¬ ∀z z = y) → (∀x(x = y → φ) → ∀z[y / x]φ))
38	22, 37	syl9 57	. . . 4 ⊢ (¬ ∀x x = y → ((¬ ∀z z = x ⋀ ¬ ∀z z = y) → ([y / x]φ → ∀z[y / x]φ)))
39	21, 38	pm2.61i 126	. . 3 ⊢ ((¬ ∀z z = x ⋀ ¬ ∀z z = y) → ([y / x]φ → ∀z[y / x]φ))
40	39	ex 373	. 2 ⊢ (¬ ∀z z = x → (¬ ∀z z = y → ([y / x]φ → ∀z[y / x]φ)))
41	9, 40	pm2.61i 126	1 ⊢ (¬ ∀z z = y → ([y / x]φ → ∀z[y / x]φ))

Syntax hints:  ¬ wn 2   → wi 3   ↔ wb 146   ⋀ wa 223  ∀wal 952   = wceq 954  [wsbc 1168

This theorem is referenced by:  hbsb4t 1247  dvelimf 1248  sbco2 1253  hbsb 1331  sbal1 1344  hbab 1465

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-8 962  ax-10 964  ax-12 966  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-10o 1138  ax-11o 1216

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 979  df-sb 1170

Copyright terms: Public domain