Theorem sbalyz 1737

Description: Move universal quantifier in and out of substitution. Identical to sbal 1738 except that it has an additional distinct variable constraint on y and z. (Contributed by Jim Kingdon, 29-Dec-2017.)

Assertion

Ref	Expression
sbalyz	⊢ ([z / y]∀xφ ↔ ∀x[z / y]φ)

Distinct variable group:   x,y,z

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

Proof of Theorem sbalyz

Step	Hyp	Ref	Expression
1		ax-ial 1358	. . . 4 ⊢ (∀xφ → ∀x∀xφ)
2	1	hbsbv 1683	. . 3 ⊢ ([z / y]∀xφ → ∀x[z / y]∀xφ)
3		ax-4 1333	. . . . 5 ⊢ (∀xφ → φ)
4	3	sbimi 1526	. . . 4 ⊢ ([z / y]∀xφ → [z / y]φ)
5	4	alimi 1275	. . 3 ⊢ (∀x[z / y]∀xφ → ∀x[z / y]φ)
6	2, 5	syl 13	. 2 ⊢ ([z / y]∀xφ → ∀x[z / y]φ)
7		sb6 1637	. . . . 5 ⊢ ([z / y]φ ↔ ∀y(y = z → φ))
8	7	albii 1290	. . . 4 ⊢ (∀x[z / y]φ ↔ ∀x∀y(y = z → φ))
9		alcom 1297	. . . 4 ⊢ (∀x∀y(y = z → φ) ↔ ∀y∀x(y = z → φ))
10	8, 9	bitri 171	. . 3 ⊢ (∀x[z / y]φ ↔ ∀y∀x(y = z → φ))
11		ax-17 1349	. . . . . 6 ⊢ (y = z → ∀x y = z)
12		alim 1277	. . . . . 6 ⊢ (∀x(y = z → φ) → (∀x y = z → ∀xφ))
13	11, 12	syl5 26	. . . . 5 ⊢ (∀x(y = z → φ) → (y = z → ∀xφ))
14	13	alimi 1275	. . . 4 ⊢ (∀y∀x(y = z → φ) → ∀y(y = z → ∀xφ))
15		sb2 1529	. . . 4 ⊢ (∀y(y = z → ∀xφ) → [z / y]∀xφ)
16	14, 15	syl 13	. . 3 ⊢ (∀y∀x(y = z → φ) → [z / y]∀xφ)
17	10, 16	sylbi 112	. 2 ⊢ (∀x[z / y]φ → [z / y]∀xφ)
18	6, 17	impbii 115	1 ⊢ ([z / y]∀xφ ↔ ∀x[z / y]φ)

Syntax hints:   → wi 4   ↔ wb 96  ∀wal 1266   = wceq 1324  [wsbc 1523

This theorem is referenced by:  sbal  1738

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 97  ax-ia2 98  ax-ia3 99  ax-5 1267  ax-7 1268  ax-gen 1269  ax-ie1 1314  ax-ie2 1315  ax-8 1328  ax-11 1330  ax-4 1333  ax-17 1349  ax-i9 1353  ax-ial 1358  ax-i5r 1359

This theorem depends on definitions:  df-bi 108  df-sb 1525