![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > cbvmpov | Structured version Visualization version GIF version |
Description: Rule to change the bound variable in a maps-to function, using implicit substitution. With a longer proof analogous to cbvmpt 5252, some distinct variable requirements could be eliminated. (Contributed by NM, 11-Jun-2013.) |
Ref | Expression |
---|---|
cbvmpov.1 | ⊢ (𝑥 = 𝑧 → 𝐶 = 𝐸) |
cbvmpov.2 | ⊢ (𝑦 = 𝑤 → 𝐸 = 𝐷) |
Ref | Expression |
---|---|
cbvmpov | ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑧 ∈ 𝐴, 𝑤 ∈ 𝐵 ↦ 𝐷) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfcv 2902 | . 2 ⊢ Ⅎ𝑧𝐶 | |
2 | nfcv 2902 | . 2 ⊢ Ⅎ𝑤𝐶 | |
3 | nfcv 2902 | . 2 ⊢ Ⅎ𝑥𝐷 | |
4 | nfcv 2902 | . 2 ⊢ Ⅎ𝑦𝐷 | |
5 | cbvmpov.1 | . . 3 ⊢ (𝑥 = 𝑧 → 𝐶 = 𝐸) | |
6 | cbvmpov.2 | . . 3 ⊢ (𝑦 = 𝑤 → 𝐸 = 𝐷) | |
7 | 5, 6 | sylan9eq 2791 | . 2 ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → 𝐶 = 𝐷) |
8 | 1, 2, 3, 4, 7 | cbvmpo 7487 | 1 ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑧 ∈ 𝐴, 𝑤 ∈ 𝐵 ↦ 𝐷) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1541 ∈ cmpo 7395 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2702 ax-sep 5292 ax-nul 5299 ax-pr 5420 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-clab 2709 df-cleq 2723 df-clel 2809 df-nfc 2884 df-rab 3432 df-v 3475 df-dif 3947 df-un 3949 df-in 3951 df-ss 3961 df-nul 4319 df-if 4523 df-sn 4623 df-pr 4625 df-op 4629 df-opab 5204 df-oprab 7397 df-mpo 7398 |
This theorem is referenced by: fvproj 8102 seqomlem0 8431 dffi3 9408 cantnfsuc 9647 fin23lem33 10322 om2uzrdg 13903 uzrdgsuci 13907 sadcp1 16378 smupp1 16403 imasvscafn 17465 mgmnsgrpex 18787 sgrpnmndex 18788 sylow1 19435 sylow2b 19455 sylow3lem5 19463 sylow3 19465 efgmval 19544 efgtf 19554 frlmphl 21269 pmatcollpw3lem 22214 mp2pm2mplem3 22239 txbas 23000 bcth 24775 opnmbl 25048 mbfimaopn 25102 mbfi1fseq 25168 motplusg 27658 ttgval 27991 ttgvalOLD 27992 opsqrlem3 31258 fedgmul 32554 mdetpmtr12 32636 madjusmdetlem4 32641 dya2iocival 33103 sxbrsigalem5 33118 sxbrsigalem6 33119 eulerpart 33212 sseqp1 33225 cvmliftlem15 34120 cvmlift2 34138 opnmbllem0 36328 mblfinlem1 36329 mblfinlem2 36330 sdc 36417 tendoplcbv 39451 dvhvaddcbv 39765 dvhvscacbv 39774 fsovcnvlem 42535 ntrneibex 42595 ioorrnopn 44794 hoidmvle 45089 ovnhoi 45092 hoimbl 45120 smflimlem6 45265 funcrngcsetc 46544 funcrngcsetcALT 46545 funcringcsetc 46581 lmod1zr 46822 functhinclem4 47312 |
Copyright terms: Public domain | W3C validator |