![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > cbvmpt2v | 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 4901, some distinct variable requirements could be eliminated. (Contributed by NM, 11-Jun-2013.) |
Ref | Expression |
---|---|
cbvmpt2v.1 | ⊢ (𝑥 = 𝑧 → 𝐶 = 𝐸) |
cbvmpt2v.2 | ⊢ (𝑦 = 𝑤 → 𝐸 = 𝐷) |
Ref | Expression |
---|---|
cbvmpt2v | ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑧 ∈ 𝐴, 𝑤 ∈ 𝐵 ↦ 𝐷) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfcv 2902 | . 2 ⊢ Ⅎ𝑧𝐶 | |
2 | nfcv 2902 | . 2 ⊢ Ⅎ𝑤𝐶 | |
3 | nfcv 2902 | . 2 ⊢ Ⅎ𝑥𝐷 | |
4 | nfcv 2902 | . 2 ⊢ Ⅎ𝑦𝐷 | |
5 | cbvmpt2v.1 | . . 3 ⊢ (𝑥 = 𝑧 → 𝐶 = 𝐸) | |
6 | cbvmpt2v.2 | . . 3 ⊢ (𝑦 = 𝑤 → 𝐸 = 𝐷) | |
7 | 5, 6 | sylan9eq 2814 | . 2 ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → 𝐶 = 𝐷) |
8 | 1, 2, 3, 4, 7 | cbvmpt2 6900 | 1 ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑧 ∈ 𝐴, 𝑤 ∈ 𝐵 ↦ 𝐷) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1632 ↦ cmpt2 6816 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1871 ax-4 1886 ax-5 1988 ax-6 2054 ax-7 2090 ax-9 2148 ax-10 2168 ax-11 2183 ax-12 2196 ax-13 2391 ax-ext 2740 ax-sep 4933 ax-nul 4941 ax-pr 5055 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-3an 1074 df-tru 1635 df-ex 1854 df-nf 1859 df-sb 2047 df-clab 2747 df-cleq 2753 df-clel 2756 df-nfc 2891 df-rab 3059 df-v 3342 df-dif 3718 df-un 3720 df-in 3722 df-ss 3729 df-nul 4059 df-if 4231 df-sn 4322 df-pr 4324 df-op 4328 df-opab 4865 df-oprab 6818 df-mpt2 6819 |
This theorem is referenced by: seqomlem0 7714 dffi3 8504 cantnfsuc 8742 fin23lem33 9379 om2uzrdg 12969 uzrdgsuci 12973 sadcp1 15399 smupp1 15424 imasvscafn 16419 mgmnsgrpex 17639 sgrpnmndex 17640 sylow1 18238 sylow2b 18258 sylow3lem5 18266 sylow3 18268 efgmval 18345 efgtf 18355 frlmphl 20342 pmatcollpw3lem 20810 mp2pm2mplem3 20835 txbas 21592 bcth 23346 opnmbl 23590 mbfimaopn 23642 mbfi1fseq 23707 motplusg 25657 ttgval 25975 opsqrlem3 29331 mdetpmtr12 30221 madjusmdetlem4 30226 fvproj 30229 dya2iocival 30665 sxbrsigalem5 30680 sxbrsigalem6 30681 eulerpart 30774 sseqp1 30787 cvmliftlem15 31608 cvmlift2 31626 opnmbllem0 33776 mblfinlem1 33777 mblfinlem2 33778 sdc 33871 tendoplcbv 36583 dvhvaddcbv 36898 dvhvscacbv 36907 fsovcnvlem 38827 ntrneibex 38891 ioorrnopn 41046 hoidmvle 41338 ovnhoi 41341 hoimbl 41369 smflimlem6 41508 funcrngcsetc 42526 funcrngcsetcALT 42527 funcringcsetc 42563 lmod1zr 42810 |
Copyright terms: Public domain | W3C validator |