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 484 | . 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐸) |
4 | mpoeq123dv.3 | . . 3 ⊢ (𝜑 → 𝐶 = 𝐹) | |
5 | 4 | adantr 484 | . 2 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → 𝐶 = 𝐹) |
6 | 1, 3, 5 | mpoeq123dva 7285 | 1 ⊢ (𝜑 → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑥 ∈ 𝐷, 𝑦 ∈ 𝐸 ↦ 𝐹)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 399 = 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-8 2112 ax-9 2120 ax-12 2175 ax-ext 2708 |
This theorem depends on definitions: df-bi 210 df-an 400 df-ex 1788 df-nf 1792 df-sb 2071 df-clab 2715 df-cleq 2729 df-clel 2816 df-oprab 7217 df-mpo 7218 |
This theorem is referenced by: mpoeq123i 7287 mptmpoopabbrd 7851 el2mpocsbcl 7853 bropopvvv 7858 bropfvvvv 7860 prdsval 16960 imasval 17016 imasvscaval 17043 homffval 17193 homfeq 17197 comfffval 17201 comffval 17202 comfffval2 17204 comffval2 17205 comfeq 17209 oppcval 17216 monfval 17237 sectffval 17255 invffval 17263 isofn 17280 cofuval 17388 natfval 17453 fucval 17466 fucco 17471 coafval 17570 setcval 17583 setcco 17589 catcval 17606 catcco 17611 estrcval 17631 estrcco 17637 xpcval 17684 1stfval 17698 2ndfval 17701 prfval 17706 evlfval 17725 evlf2 17726 curfval 17731 hofval 17760 hof2fval 17763 plusffval 18120 efmnd 18297 grpsubfval 18411 grpsubfvalALT 18412 grpsubpropd 18468 mulgfval 18490 mulgfvalALT 18491 mulgpropd 18533 lsmfval 19027 pj1fval 19084 efgtf 19112 prdsmgp 19628 dvrfval 19702 scaffval 19917 ipffval 20610 phssip 20620 frlmip 20740 psrval 20874 mamufval 21284 mvmulfval 21439 marrepfval 21457 marepvfval 21462 submafval 21476 submaval 21478 madufval 21534 minmar1fval 21543 mat2pmatfval 21620 cpm2mfval 21646 decpmatval0 21661 decpmatval 21662 pmatcollpw3lem 21680 xkoval 22484 xkopt 22552 xpstopnlem1 22706 submtmd 23001 blfvalps 23281 ishtpy 23869 isphtpy 23878 pcofval 23907 rrxip 24287 q1pval 25051 r1pval 25054 taylfval 25251 midf 26867 ismidb 26869 ttgval 26966 wwlksnon 27935 wspthsnon 27936 clwwlknonmpo 28172 grpodivfval 28615 dipfval 28783 idlsrgval 31362 submatres 31470 lmatval 31477 lmatcl 31480 qqhval 31636 sxval 31870 sitmval 32028 cndprobval 32112 mclsval 33238 csbfinxpg 35296 rrnval 35722 ldualset 36876 paddfval 37548 tgrpfset 38495 tgrpset 38496 erngfset 38550 erngset 38551 erngfset-rN 38558 erngset-rN 38559 dvafset 38755 dvaset 38756 dvhfset 38831 dvhset 38832 djaffvalN 38884 djafvalN 38885 djhffval 39147 djhfval 39148 hlhilset 39685 eldiophb 40282 mendval 40711 mnringvald 41504 mnringmulrd 41514 hoidmvval 43790 ovnhoi 43816 hspval 43822 hspmbllem2 43840 hoimbl 43844 rngcvalALTV 45192 rngccoALTV 45219 funcrngcsetcALT 45230 ringcvalALTV 45238 ringccoALTV 45282 lincop 45422 lines 45750 rrxlines 45752 spheres 45765 |
Copyright terms: Public domain | W3C validator |