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