Metamath Proof Explorer


Theorem sb8v

Description: Substitution of variable in universal quantifier. Version of sb8f with a disjoint variable condition replacing the nonfree hypothesis F/ y ph , not requiring ax-12 . (Contributed by SN, 5-Dec-2024)

Ref Expression
Assertion sb8v ( ∀ 𝑥 𝜑 ↔ ∀ 𝑦 [ 𝑦 / 𝑥 ] 𝜑 )

Proof

Step Hyp Ref Expression
1 sb6 ( [ 𝑦 / 𝑥 ] 𝜑 ↔ ∀ 𝑥 ( 𝑥 = 𝑦𝜑 ) )
2 1 albii ( ∀ 𝑦 [ 𝑦 / 𝑥 ] 𝜑 ↔ ∀ 𝑦𝑥 ( 𝑥 = 𝑦𝜑 ) )
3 alcom ( ∀ 𝑦𝑥 ( 𝑥 = 𝑦𝜑 ) ↔ ∀ 𝑥𝑦 ( 𝑥 = 𝑦𝜑 ) )
4 equcom ( 𝑥 = 𝑦𝑦 = 𝑥 )
5 4 imbi1i ( ( 𝑥 = 𝑦𝜑 ) ↔ ( 𝑦 = 𝑥𝜑 ) )
6 5 albii ( ∀ 𝑦 ( 𝑥 = 𝑦𝜑 ) ↔ ∀ 𝑦 ( 𝑦 = 𝑥𝜑 ) )
7 equsv ( ∀ 𝑦 ( 𝑦 = 𝑥𝜑 ) ↔ 𝜑 )
8 6 7 bitri ( ∀ 𝑦 ( 𝑥 = 𝑦𝜑 ) ↔ 𝜑 )
9 8 albii ( ∀ 𝑥𝑦 ( 𝑥 = 𝑦𝜑 ) ↔ ∀ 𝑥 𝜑 )
10 2 3 9 3bitrri ( ∀ 𝑥 𝜑 ↔ ∀ 𝑦 [ 𝑦 / 𝑥 ] 𝜑 )