Theorem sb8f

Description: Substitution of variable in universal quantifier. Version of sb8 with a disjoint variable condition, not requiring ax-10 or ax-13 . (Contributed by NM, 16-May-1993) (Revised by Wolf Lammen, 19-Jan-2023) Avoid ax-10 . (Revised by SN, 5-Dec-2024)

	Ref	Expression
Hypothesis	sb8f.nf	⊢ Ⅎ 𝑦 𝜑
Assertion	sb8f	⊢ ( ∀ 𝑥 𝜑 ↔ ∀ 𝑦 [ 𝑦 / 𝑥 ] 𝜑 )

Proof

Step	Hyp	Ref	Expression
1		sb8f.nf	⊢ Ⅎ 𝑦 𝜑
2		sb6	⊢ ( [ 𝑦 / 𝑥 ] 𝜑 ↔ ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) )
3	2	albii	⊢ ( ∀ 𝑦 [ 𝑦 / 𝑥 ] 𝜑 ↔ ∀ 𝑦 ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) )
4		alcom	⊢ ( ∀ 𝑦 ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ↔ ∀ 𝑥 ∀ 𝑦 ( 𝑥 = 𝑦 → 𝜑 ) )
5		sb6	⊢ ( [ 𝑥 / 𝑦 ] 𝜑 ↔ ∀ 𝑦 ( 𝑦 = 𝑥 → 𝜑 ) )
6	1	sbf	⊢ ( [ 𝑥 / 𝑦 ] 𝜑 ↔ 𝜑 )
7		equcom	⊢ ( 𝑦 = 𝑥 ↔ 𝑥 = 𝑦 )
8	7	imbi1i	⊢ ( ( 𝑦 = 𝑥 → 𝜑 ) ↔ ( 𝑥 = 𝑦 → 𝜑 ) )
9	8	albii	⊢ ( ∀ 𝑦 ( 𝑦 = 𝑥 → 𝜑 ) ↔ ∀ 𝑦 ( 𝑥 = 𝑦 → 𝜑 ) )
10	5 6 9	3bitr3ri	⊢ ( ∀ 𝑦 ( 𝑥 = 𝑦 → 𝜑 ) ↔ 𝜑 )
11	10	albii	⊢ ( ∀ 𝑥 ∀ 𝑦 ( 𝑥 = 𝑦 → 𝜑 ) ↔ ∀ 𝑥 𝜑 )
12	3 4 11	3bitrri	⊢ ( ∀ 𝑥 𝜑 ↔ ∀ 𝑦 [ 𝑦 / 𝑥 ] 𝜑 )