Description: Change bound variables in a description binder. Version of cbviotav with a disjoint variable condition, which requires fewer axioms . (Contributed by Andrew Salmon, 1-Aug-2011) (Revised by GG, 30-Sep-2024)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | cbviotavw.1 | ⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) ) | |
| Assertion | cbviotavw | ⊢ ( ℩ 𝑥 𝜑 ) = ( ℩ 𝑦 𝜓 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | cbviotavw.1 | ⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) ) | |
| 2 | 1 | cbvabv | ⊢ { 𝑥 ∣ 𝜑 } = { 𝑦 ∣ 𝜓 } |
| 3 | 2 | eqeq1i | ⊢ ( { 𝑥 ∣ 𝜑 } = { 𝑧 } ↔ { 𝑦 ∣ 𝜓 } = { 𝑧 } ) |
| 4 | 3 | abbii | ⊢ { 𝑧 ∣ { 𝑥 ∣ 𝜑 } = { 𝑧 } } = { 𝑧 ∣ { 𝑦 ∣ 𝜓 } = { 𝑧 } } |
| 5 | 4 | unieqi | ⊢ ∪ { 𝑧 ∣ { 𝑥 ∣ 𝜑 } = { 𝑧 } } = ∪ { 𝑧 ∣ { 𝑦 ∣ 𝜓 } = { 𝑧 } } |
| 6 | df-iota | ⊢ ( ℩ 𝑥 𝜑 ) = ∪ { 𝑧 ∣ { 𝑥 ∣ 𝜑 } = { 𝑧 } } | |
| 7 | df-iota | ⊢ ( ℩ 𝑦 𝜓 ) = ∪ { 𝑧 ∣ { 𝑦 ∣ 𝜓 } = { 𝑧 } } | |
| 8 | 5 6 7 | 3eqtr4i | ⊢ ( ℩ 𝑥 𝜑 ) = ( ℩ 𝑦 𝜓 ) |