Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > cbvmpt | Structured version Visualization version GIF version |
Description: Rule to change the bound variable in a maps-to function, using implicit substitution. This version has bound-variable hypotheses in place of distinct variable conditions. (Contributed by NM, 11-Sep-2011.) Add disjoint variable condition to avoid ax-13 2372. See cbvmptg 5186 for a less restrictive version requiring more axioms. (Revised by Gino Giotto, 17-Jan-2024.) |
Ref | Expression |
---|---|
cbvmpt.1 | ⊢ Ⅎ𝑦𝐵 |
cbvmpt.2 | ⊢ Ⅎ𝑥𝐶 |
cbvmpt.3 | ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶) |
Ref | Expression |
---|---|
cbvmpt | ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑦 ∈ 𝐴 ↦ 𝐶) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfcv 2907 | . 2 ⊢ Ⅎ𝑥𝐴 | |
2 | nfcv 2907 | . 2 ⊢ Ⅎ𝑦𝐴 | |
3 | cbvmpt.1 | . 2 ⊢ Ⅎ𝑦𝐵 | |
4 | cbvmpt.2 | . 2 ⊢ Ⅎ𝑥𝐶 | |
5 | cbvmpt.3 | . 2 ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶) | |
6 | 1, 2, 3, 4, 5 | cbvmptf 5183 | 1 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑦 ∈ 𝐴 ↦ 𝐶) |
Copyright terms: Public domain | W3C validator |