Theorem sbal2 1357

Description: Move quantifier in and out of substitution.

Assertion

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

Distinct variable groups:   y,z   x,z

Proof of Theorem sbal2

Step	Hyp	Ref	Expression
1		hbnae 1146	. . . 4 ⊢ (¬ ∀x x = y → ∀y ¬ ∀x x = y)
2		dveeq1 1353	. . . . . . 7 ⊢ (¬ ∀x x = y → (y = z → ∀x y = z))
3	2	19.20i 991	. . . . . 6 ⊢ (∀x ¬ ∀x x = y → ∀x(y = z → ∀x y = z))
4	3	hbnaes 1147	. . . . 5 ⊢ (¬ ∀x x = y → ∀x(y = z → ∀x y = z))
5		19.21t 1114	. . . . 5 ⊢ (∀x(y = z → ∀x y = z) → (∀x(y = z → φ) ↔ (y = z → ∀xφ)))
6	4, 5	syl 10	. . . 4 ⊢ (¬ ∀x x = y → (∀x(y = z → φ) ↔ (y = z → ∀xφ)))
7	1, 6	albid 1103	. . 3 ⊢ (¬ ∀x x = y → (∀y∀x(y = z → φ) ↔ ∀y(y = z → ∀xφ)))
8		alcom 1031	. . 3 ⊢ (∀y∀x(y = z → φ) ↔ ∀x∀y(y = z → φ))
9	7, 8	syl5rbbr 534	. 2 ⊢ (¬ ∀x x = y → (∀y(y = z → ∀xφ) ↔ ∀x∀y(y = z → φ)))
10		sb6 1266	. 2 ⊢ ([z / y]∀xφ ↔ ∀y(y = z → ∀xφ))
11		sb6 1266	. . 3 ⊢ ([z / y]φ ↔ ∀y(y = z → φ))
12	11	albii 998	. 2 ⊢ (∀x[z / y]φ ↔ ∀x∀y(y = z → φ))
13	9, 10, 12	3bitr4g 554	1 ⊢ (¬ ∀x x = y → ([z / y]∀xφ ↔ ∀x[z / y]φ))

Syntax hints:  ¬ wn 2   → wi 3   ↔ wb 146  ∀wal 953   = wceq 955  [wsbc 1169

This theorem is referenced by:  axrepndlem2 4928

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-8 963  ax-10 965  ax-12 967  ax-17 970  ax-4 972  ax-5o 974  ax-6o 977  ax-9o 1122  ax-10o 1139  ax-16 1209  ax-11o 1217

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 980  df-sb 1171

Copyright terms: Public domain