| 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 1134 | . 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵) → 𝐶 = 𝐷) |
| 3 | 2 | mpoeq3dva 7510 | 1 ⊢ (𝜑 → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐷)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 = wceq 1540 ∈ wcel 2108 ∈ cmpo 7433 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-3an 1089 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-oprab 7435 df-mpo 7436 |
| This theorem is referenced by: ofeqd 7699 seqomeq12 8494 cantnfval 9708 seqeq2 14046 seqeq3 14047 relexpsucnnr 15064 idfusubc 17945 lsmfval 19656 phssip 21676 mamuval 22397 matsc 22456 marrepval0 22567 marrepval 22568 marepvval0 22572 marepvval 22573 submaval0 22586 mdetr0 22611 mdet0 22612 mdetunilem7 22624 mdetunilem8 22625 madufval 22643 maduval 22644 maducoeval2 22646 madutpos 22648 madugsum 22649 madurid 22650 minmar1val0 22653 minmar1val 22654 pmat0opsc 22704 pmat1opsc 22705 mat2pmatval 22730 cpm2mval 22756 decpmatid 22776 pmatcollpw2lem 22783 pmatcollpw3lem 22789 mply1topmatval 22810 mp2pm2mplem1 22812 mp2pm2mplem4 22815 seqseq123d 28292 ttgval 28883 ttgvalOLD 28884 smatfval 33794 ofceq 34098 reprval 34625 finxpeq1 37387 matunitlindflem1 37623 mnringmulrvald 44246 digfval 48518 2arymaptfv 48572 itcoval 48582 dfswapf2 48967 postcofval 49059 precofval 49062 precofval2 49064 |
| Copyright terms: Public domain | W3C validator |