Description: Replace ax-10 , ax-11 , ax-12 in absn with a substitution hypothesis. (Contributed by SN, 27-May-2025)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | absnw.y | ⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) ) | |
| Assertion | absnw | ⊢ ( { 𝑥 ∣ 𝜑 } = { 𝑌 } ↔ ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑌 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | absnw.y | ⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) ) | |
| 2 | df-sn | ⊢ { 𝑌 } = { 𝑥 ∣ 𝑥 = 𝑌 } | |
| 3 | 2 | eqeq2i | ⊢ ( { 𝑥 ∣ 𝜑 } = { 𝑌 } ↔ { 𝑥 ∣ 𝜑 } = { 𝑥 ∣ 𝑥 = 𝑌 } ) |
| 4 | eqeq1 | ⊢ ( 𝑥 = 𝑦 → ( 𝑥 = 𝑌 ↔ 𝑦 = 𝑌 ) ) | |
| 5 | 1 4 | abbibw | ⊢ ( { 𝑥 ∣ 𝜑 } = { 𝑥 ∣ 𝑥 = 𝑌 } ↔ ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑌 ) ) |
| 6 | 3 5 | bitri | ⊢ ( { 𝑥 ∣ 𝜑 } = { 𝑌 } ↔ ∀ 𝑥 ( 𝜑 ↔ 𝑥 = 𝑌 ) ) |