| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > cbvmptv | Structured version Visualization version GIF version | ||
| Description: Rule to change the bound variable in a maps-to function, using implicit substitution. (Contributed by Mario Carneiro, 19-Feb-2013.) Add disjoint variable condition to avoid auxiliary axioms . See cbvmptvg 5257 for a less restrictive version requiring more axioms. (Revised by GG, 17-Nov-2024.) |
| Ref | Expression |
|---|---|
| cbvmptv.1 | ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶) |
| Ref | Expression |
|---|---|
| cbvmptv | ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑦 ∈ 𝐴 ↦ 𝐶) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | eleq1w 2824 | . . . 4 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴)) | |
| 2 | cbvmptv.1 | . . . . 5 ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶) | |
| 3 | 2 | eqeq2d 2748 | . . . 4 ⊢ (𝑥 = 𝑦 → (𝑧 = 𝐵 ↔ 𝑧 = 𝐶)) |
| 4 | 1, 3 | anbi12d 632 | . . 3 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵) ↔ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐶))) |
| 5 | 4 | cbvopab1v 5221 | . 2 ⊢ {〈𝑥, 𝑧〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵)} = {〈𝑦, 𝑧〉 ∣ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐶)} |
| 6 | df-mpt 5226 | . 2 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = {〈𝑥, 𝑧〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵)} | |
| 7 | df-mpt 5226 | . 2 ⊢ (𝑦 ∈ 𝐴 ↦ 𝐶) = {〈𝑦, 𝑧〉 ∣ (𝑦 ∈ 𝐴 ∧ 𝑧 = 𝐶)} | |
| 8 | 5, 6, 7 | 3eqtr4i 2775 | 1 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑦 ∈ 𝐴 ↦ 𝐶) |
| Copyright terms: Public domain | W3C validator |