Description: Justification theorem for df-sb proved from Tarski's FOL axiom schemes. (Contributed by BJ, 22-Jan-2023)
Ref | Expression | ||
---|---|---|---|
Assertion | sbjust | ⊢ ( ∀ 𝑦 ( 𝑦 = 𝑡 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ) ↔ ∀ 𝑧 ( 𝑧 = 𝑡 → ∀ 𝑥 ( 𝑥 = 𝑧 → 𝜑 ) ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | equequ1 | ⊢ ( 𝑦 = 𝑧 → ( 𝑦 = 𝑡 ↔ 𝑧 = 𝑡 ) ) | |
2 | equequ2 | ⊢ ( 𝑦 = 𝑧 → ( 𝑥 = 𝑦 ↔ 𝑥 = 𝑧 ) ) | |
3 | 2 | imbi1d | ⊢ ( 𝑦 = 𝑧 → ( ( 𝑥 = 𝑦 → 𝜑 ) ↔ ( 𝑥 = 𝑧 → 𝜑 ) ) ) |
4 | 3 | albidv | ⊢ ( 𝑦 = 𝑧 → ( ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ↔ ∀ 𝑥 ( 𝑥 = 𝑧 → 𝜑 ) ) ) |
5 | 1 4 | imbi12d | ⊢ ( 𝑦 = 𝑧 → ( ( 𝑦 = 𝑡 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ) ↔ ( 𝑧 = 𝑡 → ∀ 𝑥 ( 𝑥 = 𝑧 → 𝜑 ) ) ) ) |
6 | 5 | cbvalvw | ⊢ ( ∀ 𝑦 ( 𝑦 = 𝑡 → ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ) ↔ ∀ 𝑧 ( 𝑧 = 𝑡 → ∀ 𝑥 ( 𝑥 = 𝑧 → 𝜑 ) ) ) |