Theorem sbal1 996

Description: A theorem used in elimination of disjoint variable restriction on x and y by replacing it with a distinctor ¬ ∀xx = z.

Assertion

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

Distinct variable group(s):   x,y

Proof of Theorem sbal1

Step	Hyp	Ref	Expression
1		sbequ12 865	. . . . 5 ⊢ (y = z → (∀xφ ↔ [z / y]∀xφ))
2	1	a4s 682	. . . 4 ⊢ (∀y y = z → (∀xφ ↔ [z / y]∀xφ))
3		sbequ12 865	. . . . . . . 8 ⊢ (y = z → (φ ↔ [z / y]φ))
4	3	a4s 682	. . . . . . 7 ⊢ (∀y y = z → (φ ↔ [z / y]φ))
5	4	19.20i 691	. . . . . 6 ⊢ (∀x∀y y = z → ∀x(φ ↔ [z / y]φ))
6	5	eq5s 825	. . . . 5 ⊢ (∀y y = z → ∀x(φ ↔ [z / y]φ))
7		19.15 694	. . . . 5 ⊢ (∀x(φ ↔ [z / y]φ) → (∀xφ ↔ ∀x[z / y]φ))
8	6, 7	syl 12	. . . 4 ⊢ (∀y y = z → (∀xφ ↔ ∀x[z / y]φ))
9	2, 8	bitr3d 408	. . 3 ⊢ (∀y y = z → ([z / y]∀xφ ↔ ∀x[z / y]φ))
10	9	a1d 14	. 2 ⊢ (∀y y = z → (¬ ∀x x = z → ([z / y]∀xφ ↔ ∀x[z / y]φ)))
11		hba1 698	. . . . . . 7 ⊢ (∀xφ → ∀x∀xφ)
12	11	hbsb4 905	. . . . . 6 ⊢ (¬ ∀x x = z → ([z / y]∀xφ → ∀x[z / y]∀xφ))
13		ax-4 673	. . . . . . . 8 ⊢ (∀xφ → φ)
14	13	sbimi 854	. . . . . . 7 ⊢ ([z / y]∀xφ → [z / y]φ)
15	14	19.20i 691	. . . . . 6 ⊢ (∀x[z / y]∀xφ → ∀x[z / y]φ)
16	12, 15	syl6 23	. . . . 5 ⊢ (¬ ∀x x = z → ([z / y]∀xφ → ∀x[z / y]φ))
17	16	adantl 305	. . . 4 ⊢ ((¬ ∀y y = z ∧ ¬ ∀x x = z) → ([z / y]∀xφ → ∀x[z / y]φ))
18		sb4 861	. . . . . . . 8 ⊢ (¬ ∀y y = z → ([z / y]φ → ∀y(y = z → φ)))
19	18	19.20ii 692	. . . . . . 7 ⊢ (∀x ¬ ∀y y = z → (∀x[z / y]φ → ∀x∀y(y = z → φ)))
20	19	eq6s 827	. . . . . 6 ⊢ (¬ ∀y y = z → (∀x[z / y]φ → ∀x∀y(y = z → φ)))
21		ax-7 676	. . . . . 6 ⊢ (∀x∀y(y = z → φ) → ∀y∀x(y = z → φ))
22	20, 21	syl6 23	. . . . 5 ⊢ (¬ ∀y y = z → (∀x[z / y]φ → ∀y∀x(y = z → φ)))
23		ax-16 922	. . . . . . . . . . 11 ⊢ (∀x x = y → (y = z → ∀x y = z))
24	23	a1d 14	. . . . . . . . . 10 ⊢ (∀x x = y → (¬ ∀x x = z → (y = z → ∀x y = z)))
25		ax-12 802	. . . . . . . . . 10 ⊢ (¬ ∀x x = y → (¬ ∀x x = z → (y = z → ∀x y = z)))
26	24, 25	pm2.61i 110	. . . . . . . . 9 ⊢ (¬ ∀x x = z → (y = z → ∀x y = z))
27		19.20 690	. . . . . . . . 9 ⊢ (∀x(y = z → φ) → (∀x y = z → ∀xφ))
28	26, 27	syl9 55	. . . . . . . 8 ⊢ (¬ ∀x x = z → (∀x(y = z → φ) → (y = z → ∀xφ)))
29	28	19.20ii 692	. . . . . . 7 ⊢ (∀y ¬ ∀x x = z → (∀y∀x(y = z → φ) → ∀y(y = z → ∀xφ)))
30		sb2 859	. . . . . . 7 ⊢ (∀y(y = z → ∀xφ) → [z / y]∀xφ)
31	29, 30	syl6 23	. . . . . 6 ⊢ (∀y ¬ ∀x x = z → (∀y∀x(y = z → φ) → [z / y]∀xφ))
32	31	eq6s 827	. . . . 5 ⊢ (¬ ∀x x = z → (∀y∀x(y = z → φ) → [z / y]∀xφ))
33	22, 32	sylan9 359	. . . 4 ⊢ ((¬ ∀y y = z ∧ ¬ ∀x x = z) → (∀x[z / y]φ → [z / y]∀xφ))
34	17, 33	impbid 397	. . 3 ⊢ ((¬ ∀y y = z ∧ ¬ ∀x x = z) → ([z / y]∀xφ ↔ ∀x[z / y]φ))
35	34	exp 291	. 2 ⊢ (¬ ∀y y = z → (¬ ∀x x = z → ([z / y]∀xφ ↔ ∀x[z / y]φ)))
36	10, 35	pm2.61i 110	1 ⊢ (¬ ∀x x = z → ([z / y]∀xφ ↔ ∀x[z / y]φ))

Syntax hints:  ¬ wn 1   → wi 2   ↔ wb 127   ∧ wa 196  ∀wal 672   = weq 797  [wsb 852

This theorem is referenced by:  sbal 997

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-16 922

This theorem depends on definitions:  df-bi 128  df-an 198  df-ex 679  df-sb 853

metamath.org