![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > cbvmptv | GIF version |
Description: Rule to change the bound variable in a maps-to function, using implicit substitution. (Contributed by Mario Carneiro, 19-Feb-2013.) |
Ref | Expression |
---|---|
cbvmptv.1 | ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶) |
Ref | Expression |
---|---|
cbvmptv | ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑦 ∈ 𝐴 ↦ 𝐶) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfcv 2255 | . 2 ⊢ Ⅎ𝑦𝐵 | |
2 | nfcv 2255 | . 2 ⊢ Ⅎ𝑥𝐶 | |
3 | cbvmptv.1 | . 2 ⊢ (𝑥 = 𝑦 → 𝐵 = 𝐶) | |
4 | 1, 2, 3 | cbvmpt 3983 | 1 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑦 ∈ 𝐴 ↦ 𝐶) |
Colors of variables: wff set class |
Syntax hints: → wi 4 = wceq 1314 ↦ cmpt 3949 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-io 681 ax-5 1406 ax-7 1407 ax-gen 1408 ax-ie1 1452 ax-ie2 1453 ax-8 1465 ax-10 1466 ax-11 1467 ax-i12 1468 ax-bndl 1469 ax-4 1470 ax-17 1489 ax-i9 1493 ax-ial 1497 ax-i5r 1498 ax-ext 2097 |
This theorem depends on definitions: df-bi 116 df-3an 947 df-tru 1317 df-nf 1420 df-sb 1719 df-clab 2102 df-cleq 2108 df-clel 2111 df-nfc 2244 df-v 2659 df-un 3041 df-sn 3499 df-pr 3500 df-op 3502 df-opab 3950 df-mpt 3951 |
This theorem is referenced by: frecsuc 6258 xpmapen 6697 omp1eom 6932 fodjuomni 6971 fodjumkv 6984 caucvgsrlembnd 7540 negiso 8620 infrenegsupex 9288 frec2uzsucd 10064 frecuzrdgdom 10081 frecuzrdgfun 10083 frecuzrdgsuct 10087 0tonninf 10102 1tonninf 10103 seq3f1oleml 10166 seq3f1o 10167 hashfz1 10419 xrnegiso 10920 infxrnegsupex 10921 climcvg1n 11008 summodc 11041 zsumdc 11042 fsum3 11045 fsumadd 11064 phimullem 11743 ennnfonelemnn0 11777 ennnfonelemr 11778 ctinfom 11783 cdivcncfap 12570 expcncf 12575 subctctexmid 12880 nninfsellemqall 12895 nninfomni 12899 nninffeq 12900 exmidsbthrlem 12901 exmidsbthr 12902 isomninn 12910 |
Copyright terms: Public domain | W3C validator |