Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > mpoeq3dv | Structured version Visualization version GIF version |
Description: An equality deduction for the maps-to notation restricted to the value of the operation. (Contributed by SO, 16-Jul-2018.) |
Ref | Expression |
---|---|
mpoeq3dv.1 | ⊢ (𝜑 → 𝐶 = 𝐷) |
Ref | Expression |
---|---|
mpoeq3dv | ⊢ (𝜑 → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐷)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mpoeq3dv.1 | . . 3 ⊢ (𝜑 → 𝐶 = 𝐷) | |
2 | 1 | 3ad2ant1 1135 | . 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝐶 = 𝐷) |
3 | 2 | mpoeq3dva 7288 | 1 ⊢ (𝜑 → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐷)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1543 ∈ wcel 2110 ∈ cmpo 7215 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2016 ax-9 2120 ax-12 2175 ax-ext 2708 |
This theorem depends on definitions: df-bi 210 df-an 400 df-3an 1091 df-ex 1788 df-nf 1792 df-sb 2071 df-clab 2715 df-cleq 2729 df-oprab 7217 df-mpo 7218 |
This theorem is referenced by: seqomeq12 8190 cantnfval 9283 seqeq2 13578 seqeq3 13579 relexpsucnnr 14588 lsmfval 19027 phssip 20620 mamuval 21285 matsc 21347 marrepval0 21458 marrepval 21459 marepvval0 21463 marepvval 21464 submaval0 21477 mdetr0 21502 mdet0 21503 mdetunilem7 21515 mdetunilem8 21516 madufval 21534 maduval 21535 maducoeval2 21537 madutpos 21539 madugsum 21540 madurid 21541 minmar1val0 21544 minmar1val 21545 pmat0opsc 21595 pmat1opsc 21596 mat2pmatval 21621 cpm2mval 21647 decpmatid 21667 pmatcollpw2lem 21674 pmatcollpw3lem 21680 mply1topmatval 21701 mp2pm2mplem1 21703 mp2pm2mplem4 21706 ttgval 26966 smatfval 31459 ofceq 31777 reprval 32302 finxpeq1 35294 matunitlindflem1 35510 mnringmulrvald 41518 idfusubc 45097 digfval 45616 2arymaptfv 45670 itcoval 45680 |
Copyright terms: Public domain | W3C validator |