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