![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > mpoeq123dv | Structured version Visualization version GIF version |
Description: An equality deduction for the maps-to notation. (Contributed by NM, 12-Sep-2011.) |
Ref | Expression |
---|---|
mpoeq123dv.1 | ⊢ (𝜑 → 𝐴 = 𝐷) |
mpoeq123dv.2 | ⊢ (𝜑 → 𝐵 = 𝐸) |
mpoeq123dv.3 | ⊢ (𝜑 → 𝐶 = 𝐹) |
Ref | Expression |
---|---|
mpoeq123dv | ⊢ (𝜑 → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑥 ∈ 𝐷, 𝑦 ∈ 𝐸 ↦ 𝐹)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mpoeq123dv.1 | . 2 ⊢ (𝜑 → 𝐴 = 𝐷) | |
2 | mpoeq123dv.2 | . . 3 ⊢ (𝜑 → 𝐵 = 𝐸) | |
3 | 2 | adantr 479 | . 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐸) |
4 | mpoeq123dv.3 | . . 3 ⊢ (𝜑 → 𝐶 = 𝐹) | |
5 | 4 | adantr 479 | . 2 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → 𝐶 = 𝐹) |
6 | 1, 3, 5 | mpoeq123dva 7499 | 1 ⊢ (𝜑 → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑥 ∈ 𝐷, 𝑦 ∈ 𝐸 ↦ 𝐹)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 394 = wceq 1534 ∈ wcel 2099 ∈ cmpo 7426 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-ext 2697 |
This theorem depends on definitions: df-bi 206 df-an 395 df-ex 1775 df-sb 2061 df-clab 2704 df-cleq 2718 df-clel 2803 df-oprab 7428 df-mpo 7429 |
This theorem is referenced by: mpoeq123i 7501 mptmpoopabbrd 8094 mptmpoopabbrdOLD 8095 mptmpoopabbrdOLDOLD 8097 el2mpocsbcl 8099 bropopvvv 8104 bropfvvvv 8106 prdsval 17470 imasval 17526 imasvscaval 17553 homffval 17703 homfeq 17707 comfffval 17711 comffval 17712 comfffval2 17714 comffval2 17715 comfeq 17719 oppcval 17726 monfval 17748 sectffval 17766 invffval 17774 isofn 17791 cofuval 17901 natfval 17969 fucval 17982 fucco 17987 coafval 18086 setcval 18099 setcco 18105 catcval 18122 catcco 18127 estrcval 18147 estrcco 18153 xpcval 18201 1stfval 18215 2ndfval 18218 prfval 18223 evlfval 18242 evlf2 18243 curfval 18248 hofval 18277 hof2fval 18280 plusffval 18639 efmnd 18860 grpsubfval 18978 grpsubfvalALT 18979 grpsubpropd 19039 mulgfval 19063 mulgfvalALT 19064 mulgpropd 19110 lsmfval 19636 pj1fval 19692 efgtf 19720 prdsmgp 20134 dvrfval 20384 funcrngcsetcALT 20619 scaffval 20856 ipffval 21644 phssip 21654 frlmip 21776 psrval 21912 mamufval 22383 mvmulfval 22535 marrepfval 22553 marepvfval 22558 submafval 22572 submaval 22574 madufval 22630 minmar1fval 22639 mat2pmatfval 22716 cpm2mfval 22742 decpmatval0 22757 decpmatval 22758 pmatcollpw3lem 22776 xkoval 23582 xkopt 23650 xpstopnlem1 23804 submtmd 24099 blfvalps 24380 ishtpy 24989 isphtpy 24998 pcofval 25028 rrxip 25409 q1pval 26182 r1pval 26185 taylfval 26386 istrkgl 28385 midf 28703 ismidb 28705 ttgval 28802 ttgvalOLD 28803 wwlksnon 29785 wspthsnon 29786 clwwlknonmpo 30022 grpodivfval 30467 dipfval 30635 rlocval 33114 idlsrgval 33378 submatres 33621 lmatval 33628 lmatcl 33631 qqhval 33789 sxval 34023 sitmval 34183 cndprobval 34267 mclsval 35391 csbfinxpg 37095 rrnval 37528 ldualset 38823 paddfval 39496 tgrpfset 40443 tgrpset 40444 erngfset 40498 erngset 40499 erngfset-rN 40506 erngset-rN 40507 dvafset 40703 dvaset 40704 dvhfset 40779 dvhset 40780 djaffvalN 40832 djafvalN 40833 djhffval 41095 djhfval 41096 hlhilset 41633 eldiophb 42414 mendval 42844 mnringvald 43882 mnringmulrd 43895 hoidmvval 46198 ovnhoi 46224 hspval 46230 hspmbllem2 46248 hoimbl 46252 rngcvalALTV 47642 rngccoALTV 47648 ringcvalALTV 47666 ringccoALTV 47682 lincop 47791 lines 48119 rrxlines 48121 spheres 48134 |
Copyright terms: Public domain | W3C validator |