Theorem sbal

Description: Move universal quantifier in and out of substitution. (Contributed by NM, 16-May-1993) (Proof shortened by Wolf Lammen, 29-Sep-2018) Reduce dependencies on axioms. (Revised by Steven Nguyen, 13-Aug-2023)

	Ref	Expression
Assertion	sbal	⊢ ( [ 𝑧 / 𝑦 ] ∀ 𝑥 𝜑 ↔ ∀ 𝑥 [ 𝑧 / 𝑦 ] 𝜑 )

Proof

Step	Hyp	Ref	Expression
1		alcom	⊢ ( ∀ 𝑤 ∀ 𝑥 ( 𝑤 = 𝑧 → ∀ 𝑦 ( 𝑦 = 𝑤 → 𝜑 ) ) ↔ ∀ 𝑥 ∀ 𝑤 ( 𝑤 = 𝑧 → ∀ 𝑦 ( 𝑦 = 𝑤 → 𝜑 ) ) )
2		19.21v	⊢ ( ∀ 𝑥 ( 𝑦 = 𝑤 → 𝜑 ) ↔ ( 𝑦 = 𝑤 → ∀ 𝑥 𝜑 ) )
3	2	albii	⊢ ( ∀ 𝑦 ∀ 𝑥 ( 𝑦 = 𝑤 → 𝜑 ) ↔ ∀ 𝑦 ( 𝑦 = 𝑤 → ∀ 𝑥 𝜑 ) )
4		alcom	⊢ ( ∀ 𝑦 ∀ 𝑥 ( 𝑦 = 𝑤 → 𝜑 ) ↔ ∀ 𝑥 ∀ 𝑦 ( 𝑦 = 𝑤 → 𝜑 ) )
5	3 4	bitr3i	⊢ ( ∀ 𝑦 ( 𝑦 = 𝑤 → ∀ 𝑥 𝜑 ) ↔ ∀ 𝑥 ∀ 𝑦 ( 𝑦 = 𝑤 → 𝜑 ) )
6	5	imbi2i	⊢ ( ( 𝑤 = 𝑧 → ∀ 𝑦 ( 𝑦 = 𝑤 → ∀ 𝑥 𝜑 ) ) ↔ ( 𝑤 = 𝑧 → ∀ 𝑥 ∀ 𝑦 ( 𝑦 = 𝑤 → 𝜑 ) ) )
7	6	albii	⊢ ( ∀ 𝑤 ( 𝑤 = 𝑧 → ∀ 𝑦 ( 𝑦 = 𝑤 → ∀ 𝑥 𝜑 ) ) ↔ ∀ 𝑤 ( 𝑤 = 𝑧 → ∀ 𝑥 ∀ 𝑦 ( 𝑦 = 𝑤 → 𝜑 ) ) )
8		df-sb	⊢ ( [ 𝑧 / 𝑦 ] ∀ 𝑥 𝜑 ↔ ∀ 𝑤 ( 𝑤 = 𝑧 → ∀ 𝑦 ( 𝑦 = 𝑤 → ∀ 𝑥 𝜑 ) ) )
9		19.21v	⊢ ( ∀ 𝑥 ( 𝑤 = 𝑧 → ∀ 𝑦 ( 𝑦 = 𝑤 → 𝜑 ) ) ↔ ( 𝑤 = 𝑧 → ∀ 𝑥 ∀ 𝑦 ( 𝑦 = 𝑤 → 𝜑 ) ) )
10	9	albii	⊢ ( ∀ 𝑤 ∀ 𝑥 ( 𝑤 = 𝑧 → ∀ 𝑦 ( 𝑦 = 𝑤 → 𝜑 ) ) ↔ ∀ 𝑤 ( 𝑤 = 𝑧 → ∀ 𝑥 ∀ 𝑦 ( 𝑦 = 𝑤 → 𝜑 ) ) )
11	7 8 10	3bitr4i	⊢ ( [ 𝑧 / 𝑦 ] ∀ 𝑥 𝜑 ↔ ∀ 𝑤 ∀ 𝑥 ( 𝑤 = 𝑧 → ∀ 𝑦 ( 𝑦 = 𝑤 → 𝜑 ) ) )
12		df-sb	⊢ ( [ 𝑧 / 𝑦 ] 𝜑 ↔ ∀ 𝑤 ( 𝑤 = 𝑧 → ∀ 𝑦 ( 𝑦 = 𝑤 → 𝜑 ) ) )
13	12	albii	⊢ ( ∀ 𝑥 [ 𝑧 / 𝑦 ] 𝜑 ↔ ∀ 𝑥 ∀ 𝑤 ( 𝑤 = 𝑧 → ∀ 𝑦 ( 𝑦 = 𝑤 → 𝜑 ) ) )
14	1 11 13	3bitr4i	⊢ ( [ 𝑧 / 𝑦 ] ∀ 𝑥 𝜑 ↔ ∀ 𝑥 [ 𝑧 / 𝑦 ] 𝜑 )