![]() |
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 1126 | . 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝐶 = 𝐷) |
3 | 2 | mpoeq3dva 7092 | 1 ⊢ (𝜑 → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐷)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1522 ∈ wcel 2080 ∈ cmpo 7021 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1778 ax-4 1792 ax-5 1889 ax-6 1948 ax-7 1993 ax-9 2090 ax-12 2140 ax-ext 2768 |
This theorem depends on definitions: df-bi 208 df-an 397 df-3an 1082 df-ex 1763 df-nf 1767 df-sb 2042 df-clab 2775 df-cleq 2787 df-oprab 7023 df-mpo 7024 |
This theorem is referenced by: seqomeq12 7944 cantnfval 8980 seqeq2 13223 seqeq3 13224 relexpsucnnr 14218 lsmfval 18493 phssip 20484 mamuval 20679 matsc 20743 marrepval0 20854 marrepval 20855 marepvval0 20859 marepvval 20860 submaval0 20873 mdetr0 20898 mdet0 20899 mdetunilem7 20911 mdetunilem8 20912 madufval 20930 maduval 20931 maducoeval2 20933 madutpos 20935 madugsum 20936 madurid 20937 minmar1val0 20940 minmar1val 20941 pmat0opsc 20990 pmat1opsc 20991 mat2pmatval 21016 cpm2mval 21042 decpmatid 21062 pmatcollpw2lem 21069 pmatcollpw3lem 21075 mply1topmatval 21096 mp2pm2mplem1 21098 mp2pm2mplem4 21101 ttgval 26344 smatfval 30667 ofceq 30965 reprval 31490 finxpeq1 34211 matunitlindflem1 34432 idfusubc 43629 digfval 44152 |
Copyright terms: Public domain | W3C validator |