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