![]() |
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 1132 | . 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝐶 = 𝐷) |
3 | 2 | mpoeq3dva 7489 | 1 ⊢ (𝜑 → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐷)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1540 ∈ wcel 2105 ∈ cmpo 7414 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1912 ax-6 1970 ax-7 2010 ax-9 2115 ax-ext 2702 |
This theorem depends on definitions: df-bi 206 df-an 396 df-3an 1088 df-ex 1781 df-sb 2067 df-clab 2709 df-cleq 2723 df-oprab 7416 df-mpo 7417 |
This theorem is referenced by: ofeqd 7676 seqomeq12 8460 cantnfval 9669 seqeq2 13977 seqeq3 13978 relexpsucnnr 14979 idfusubc 17857 lsmfval 19554 phssip 21520 mamuval 22207 matsc 22271 marrepval0 22382 marrepval 22383 marepvval0 22387 marepvval 22388 submaval0 22401 mdetr0 22426 mdet0 22427 mdetunilem7 22439 mdetunilem8 22440 madufval 22458 maduval 22459 maducoeval2 22461 madutpos 22463 madugsum 22464 madurid 22465 minmar1val0 22468 minmar1val 22469 pmat0opsc 22519 pmat1opsc 22520 mat2pmatval 22545 cpm2mval 22571 decpmatid 22591 pmatcollpw2lem 22598 pmatcollpw3lem 22604 mply1topmatval 22625 mp2pm2mplem1 22627 mp2pm2mplem4 22630 ttgval 28558 ttgvalOLD 28559 smatfval 33238 ofceq 33558 reprval 34085 finxpeq1 36730 matunitlindflem1 36947 mnringmulrvald 43448 digfval 47444 2arymaptfv 47498 itcoval 47508 |
Copyright terms: Public domain | W3C validator |