![]() |
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 5259, 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 | eleq1w 2822 | . . . . 5 ⊢ (𝑥 = 𝑧 → (𝑥 ∈ 𝐴 ↔ 𝑧 ∈ 𝐴)) | |
2 | eleq1w 2822 | . . . . 5 ⊢ (𝑦 = 𝑤 → (𝑦 ∈ 𝐵 ↔ 𝑤 ∈ 𝐵)) | |
3 | 1, 2 | bi2anan9 638 | . . . 4 ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ↔ (𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵))) |
4 | cbvmpov.1 | . . . . . 6 ⊢ (𝑥 = 𝑧 → 𝐶 = 𝐸) | |
5 | cbvmpov.2 | . . . . . 6 ⊢ (𝑦 = 𝑤 → 𝐸 = 𝐷) | |
6 | 4, 5 | sylan9eq 2795 | . . . . 5 ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → 𝐶 = 𝐷) |
7 | 6 | eqeq2d 2746 | . . . 4 ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (𝑣 = 𝐶 ↔ 𝑣 = 𝐷)) |
8 | 3, 7 | anbi12d 632 | . . 3 ⊢ ((𝑥 = 𝑧 ∧ 𝑦 = 𝑤) → (((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑣 = 𝐶) ↔ ((𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵) ∧ 𝑣 = 𝐷))) |
9 | 8 | cbvoprab12v 7523 | . 2 ⊢ {〈〈𝑥, 𝑦〉, 𝑣〉 ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑣 = 𝐶)} = {〈〈𝑧, 𝑤〉, 𝑣〉 ∣ ((𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵) ∧ 𝑣 = 𝐷)} |
10 | df-mpo 7436 | . 2 ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = {〈〈𝑥, 𝑦〉, 𝑣〉 ∣ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) ∧ 𝑣 = 𝐶)} | |
11 | df-mpo 7436 | . 2 ⊢ (𝑧 ∈ 𝐴, 𝑤 ∈ 𝐵 ↦ 𝐷) = {〈〈𝑧, 𝑤〉, 𝑣〉 ∣ ((𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐵) ∧ 𝑣 = 𝐷)} | |
12 | 9, 10, 11 | 3eqtr4i 2773 | 1 ⊢ (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑧 ∈ 𝐴, 𝑤 ∈ 𝐵 ↦ 𝐷) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 395 = wceq 1537 ∈ wcel 2106 {coprab 7432 ∈ cmpo 7433 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1908 ax-6 1965 ax-7 2005 ax-8 2108 ax-9 2116 ax-ext 2706 |
This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1540 df-fal 1550 df-ex 1777 df-sb 2063 df-clab 2713 df-cleq 2727 df-clel 2814 df-rab 3434 df-v 3480 df-dif 3966 df-un 3968 df-ss 3980 df-nul 4340 df-if 4532 df-sn 4632 df-pr 4634 df-op 4638 df-oprab 7435 df-mpo 7436 |
This theorem is referenced by: fvproj 8158 seqomlem0 8488 dffi3 9469 cantnfsuc 9708 fin23lem33 10383 om2uzrdg 13994 uzrdgsuci 13998 sadcp1 16489 smupp1 16514 imasvscafn 17584 mgmnsgrpex 18957 sgrpnmndex 18958 sylow1 19636 sylow2b 19656 sylow3lem5 19664 sylow3 19666 efgmval 19745 efgtf 19755 funcrngcsetc 20657 funcrngcsetcALT 20658 funcringcsetc 20691 frlmphl 21819 pmatcollpw3lem 22805 mp2pm2mplem3 22830 txbas 23591 mpomulcn 24905 bcth 25377 opnmbl 25651 mbfimaopn 25705 mbfi1fseq 25771 om2noseqrdg 28325 noseqrdgsuc 28329 motplusg 28565 ttgval 28898 ttgvalOLD 28899 opsqrlem3 32171 elrgspnlem2 33233 fedgmul 33659 mdetpmtr12 33786 madjusmdetlem4 33791 dya2iocival 34255 sxbrsigalem5 34270 sxbrsigalem6 34271 eulerpart 34364 sseqp1 34377 cvmliftlem15 35283 cvmlift2 35301 opnmbllem0 37643 mblfinlem1 37644 mblfinlem2 37645 sdc 37731 tendoplcbv 40758 dvhvaddcbv 41072 dvhvscacbv 41081 fsovcnvlem 44003 ntrneibex 44063 ioorrnopn 46261 hoidmvle 46556 ovnhoi 46559 hoimbl 46587 smflimlem6 46732 lmod1zr 48339 functhinclem4 48844 |
Copyright terms: Public domain | W3C validator |