Metamath Proof Explorer


Theorem hbsbwOLD

Description: Obsolete version of hbsbw as of 14-May-2025. (Contributed by NM, 12-Aug-1993) (Revised by Gino Giotto, 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 df-sb ( [ 𝑦 / 𝑥 ] 𝜑 ↔ ∀ 𝑤 ( 𝑤 = 𝑦 → ∀ 𝑥 ( 𝑥 = 𝑤𝜑 ) ) )
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 ( [ 𝑦 / 𝑥 ] 𝜑 → ∀ 𝑧 [ 𝑦 / 𝑥 ] 𝜑 )