![]() |
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 481 | . 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐸) |
4 | mpoeq123dv.3 | . . 3 ⊢ (𝜑 → 𝐶 = 𝐹) | |
5 | 4 | adantr 481 | . 2 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → 𝐶 = 𝐹) |
6 | 1, 3, 5 | mpoeq123dva 7086 | 1 ⊢ (𝜑 → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑥 ∈ 𝐷, 𝑦 ∈ 𝐸 ↦ 𝐹)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 = wceq 1522 ∈ wcel 2081 ∈ cmpo 7018 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1777 ax-4 1791 ax-5 1888 ax-6 1947 ax-7 1992 ax-8 2083 ax-9 2091 ax-12 2141 ax-ext 2769 |
This theorem depends on definitions: df-bi 208 df-an 397 df-ex 1762 df-nf 1766 df-sb 2043 df-clab 2776 df-cleq 2788 df-clel 2863 df-oprab 7020 df-mpo 7021 |
This theorem is referenced by: mpoeq123i 7088 mptmpoopabbrd 7634 el2mpocsbcl 7636 bropopvvv 7641 bropfvvvv 7643 prdsval 16557 imasval 16613 imasvscaval 16640 homffval 16789 homfeq 16793 comfffval 16797 comffval 16798 comfffval2 16800 comffval2 16801 comfeq 16805 oppcval 16812 monfval 16831 sectffval 16849 invffval 16857 isofn 16874 cofuval 16981 natfval 17045 fucval 17057 fucco 17061 coafval 17153 setcval 17166 setcco 17172 catcval 17185 catcco 17190 estrcval 17203 estrcco 17209 xpcval 17256 xpchomfval 17258 xpccofval 17261 1stfval 17270 2ndfval 17273 prfval 17278 evlfval 17296 evlf2 17297 curfval 17302 hofval 17331 hof2fval 17334 plusffval 17686 grpsubfval 17904 grpsubfvalALT 17905 grpsubpropd 17961 mulgfval 17983 mulgfvalALT 17984 mulgpropd 18023 symgval 18238 lsmfval 18493 pj1fval 18547 efgtf 18575 prdsmgp 19050 dvrfval 19124 scaffval 19342 psrval 19830 ipffval 20474 phssip 20484 frlmip 20604 mamufval 20678 mvmulfval 20835 marrepfval 20853 marepvfval 20858 submafval 20872 submaval 20874 madufval 20930 minmar1fval 20939 mat2pmatfval 21015 cpm2mfval 21041 decpmatval0 21056 decpmatval 21057 pmatcollpw3lem 21075 xkoval 21879 xkopt 21947 xpstopnlem1 22101 submtmd 22396 blfvalps 22676 ishtpy 23259 isphtpy 23268 pcofval 23297 rrxip 23676 q1pval 24430 r1pval 24433 taylfval 24630 midf 26244 ismidb 26246 ttgval 26344 wwlksnon 27316 wspthsnon 27317 clwwlknonmpo 27555 grpodivfval 28002 dipfval 28170 submatres 30686 lmatval 30693 lmatcl 30696 qqhval 30832 sxval 31066 sitmval 31224 cndprobval 31308 mclsval 32419 csbfinxpg 34219 rrnval 34656 ldualset 35811 paddfval 36483 tgrpfset 37430 tgrpset 37431 erngfset 37485 erngset 37486 erngfset-rN 37493 erngset-rN 37494 dvafset 37690 dvaset 37691 dvhfset 37766 dvhset 37767 djaffvalN 37819 djafvalN 37820 djhffval 38082 djhfval 38083 hlhilset 38620 eldiophb 38858 mendval 39287 hoidmvval 42421 ovnhoi 42447 hspval 42453 hspmbllem2 42471 hoimbl 42475 rngcvalALTV 43730 rngccoALTV 43757 funcrngcsetcALT 43768 ringcvalALTV 43776 ringccoALTV 43820 lincop 43963 lines 44219 rrxlines 44221 spheres 44234 |
Copyright terms: Public domain | W3C validator |