Metamath Proof Explorer


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