This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 dfsb ⊢ ( [ 𝑧 / 𝑦 ] ∀ 𝑥 𝜑 ↔ ∀ 𝑤 ( 𝑤 = 𝑧 → ∀ 𝑦 ( 𝑦 = 𝑤 → ∀ 𝑥 𝜑 ) ) )
9 19.21v ⊢ ( ∀ 𝑥 ( 𝑤 = 𝑧 → ∀ 𝑦 ( 𝑦 = 𝑤 → 𝜑 ) ) ↔ ( 𝑤 = 𝑧 → ∀ 𝑥 ∀ 𝑦 ( 𝑦 = 𝑤 → 𝜑 ) ) )
10 9 albii ⊢ ( ∀ 𝑤 ∀ 𝑥 ( 𝑤 = 𝑧 → ∀ 𝑦 ( 𝑦 = 𝑤 → 𝜑 ) ) ↔ ∀ 𝑤 ( 𝑤 = 𝑧 → ∀ 𝑥 ∀ 𝑦 ( 𝑦 = 𝑤 → 𝜑 ) ) )
11 7 8 10 3bitr4i ⊢ ( [ 𝑧 / 𝑦 ] ∀ 𝑥 𝜑 ↔ ∀ 𝑤 ∀ 𝑥 ( 𝑤 = 𝑧 → ∀ 𝑦 ( 𝑦 = 𝑤 → 𝜑 ) ) )
12 dfsb ⊢ ( [ 𝑧 / 𝑦 ] 𝜑 ↔ ∀ 𝑤 ( 𝑤 = 𝑧 → ∀ 𝑦 ( 𝑦 = 𝑤 → 𝜑 ) ) )
13 12 albii ⊢ ( ∀ 𝑥 [ 𝑧 / 𝑦 ] 𝜑 ↔ ∀ 𝑥 ∀ 𝑤 ( 𝑤 = 𝑧 → ∀ 𝑦 ( 𝑦 = 𝑤 → 𝜑 ) ) )
14 1 11 13 3bitr4i ⊢ ( [ 𝑧 / 𝑦 ] ∀ 𝑥 𝜑 ↔ ∀ 𝑥 [ 𝑧 / 𝑦 ] 𝜑 )