Theorem hbsbw

Description: If z is not free in ph , it is not free in [ y / x ] ph when y and z are distinct. Version of hbsb with a disjoint variable condition, which requires fewer axioms. (Contributed by NM, 12-Aug-1993) (Revised by Gino Giotto, 23-May-2024)

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

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	⊢ ( [ 𝑦 / 𝑥 ] 𝜑 → ∀ 𝑧 [ 𝑦 / 𝑥 ] 𝜑 )