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

Metamath Proof Explorer

Theorem hbsbwOLD

Description: Obsolete version of hbsbw as of 14-May-2025. (Contributed by NM, 12-Aug-1993) (Revised by GG, 23-May-2024) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Hypothesis hbsbw.1 ⊢ ( 𝜑 → ∀ 𝑧 𝜑 )
Assertion hbsbwOLD ( [ 𝑦 / 𝑥 ] 𝜑 → ∀ 𝑧 [ 𝑦 / 𝑥 ] 𝜑 )

Proof

Step Hyp Ref Expression
1 hbsbw.1 ⊢ ( 𝜑 → ∀ 𝑧 𝜑 )
2 dfsb ⊢ ( [ 𝑦 / 𝑥 ] 𝜑 ↔ ∀ 𝑤 ( 𝑤 = 𝑦 → ∀ 𝑥 ( 𝑥 = 𝑤 → 𝜑 ) ) )
3 1 imim2i ⊢ ( ( 𝑥 = 𝑤 → 𝜑 ) → ( 𝑥 = 𝑤 → ∀ 𝑧 𝜑 ) )
4 3 alimi ⊢ ( ∀ 𝑥 ( 𝑥 = 𝑤 → 𝜑 ) → ∀ 𝑥 ( 𝑥 = 𝑤 → ∀ 𝑧 𝜑 ) )
5 19.21v ⊢ ( ∀ 𝑧 ( 𝑥 = 𝑤 → 𝜑 ) ↔ ( 𝑥 = 𝑤 → ∀ 𝑧 𝜑 ) )
6 5 biimpri ⊢ ( ( 𝑥 = 𝑤 → ∀ 𝑧 𝜑 ) → ∀ 𝑧 ( 𝑥 = 𝑤 → 𝜑 ) )
7 6 alimi ⊢ ( ∀ 𝑥 ( 𝑥 = 𝑤 → ∀ 𝑧 𝜑 ) → ∀ 𝑥 ∀ 𝑧 ( 𝑥 = 𝑤 → 𝜑 ) )
8 ax-11 ⊢ ( ∀ 𝑥 ∀ 𝑧 ( 𝑥 = 𝑤 → 𝜑 ) → ∀ 𝑧 ∀ 𝑥 ( 𝑥 = 𝑤 → 𝜑 ) )
9 4 7 8 3syl ⊢ ( ∀ 𝑥 ( 𝑥 = 𝑤 → 𝜑 ) → ∀ 𝑧 ∀ 𝑥 ( 𝑥 = 𝑤 → 𝜑 ) )
10 9 imim2i ⊢ ( ( 𝑤 = 𝑦 → ∀ 𝑥 ( 𝑥 = 𝑤 → 𝜑 ) ) → ( 𝑤 = 𝑦 → ∀ 𝑧 ∀ 𝑥 ( 𝑥 = 𝑤 → 𝜑 ) ) )
11 19.21v ⊢ ( ∀ 𝑧 ( 𝑤 = 𝑦 → ∀ 𝑥 ( 𝑥 = 𝑤 → 𝜑 ) ) ↔ ( 𝑤 = 𝑦 → ∀ 𝑧 ∀ 𝑥 ( 𝑥 = 𝑤 → 𝜑 ) ) )
12 10 11 sylibr ⊢ ( ( 𝑤 = 𝑦 → ∀ 𝑥 ( 𝑥 = 𝑤 → 𝜑 ) ) → ∀ 𝑧 ( 𝑤 = 𝑦 → ∀ 𝑥 ( 𝑥 = 𝑤 → 𝜑 ) ) )
13 12 hbal ⊢ ( ∀ 𝑤 ( 𝑤 = 𝑦 → ∀ 𝑥 ( 𝑥 = 𝑤 → 𝜑 ) ) → ∀ 𝑧 ∀ 𝑤 ( 𝑤 = 𝑦 → ∀ 𝑥 ( 𝑥 = 𝑤 → 𝜑 ) ) )
14 2 13 hbxfrbi ⊢ ( [ 𝑦 / 𝑥 ] 𝜑 → ∀ 𝑧 [ 𝑦 / 𝑥 ] 𝜑 )