![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > mpt2eq123dv | Structured version Visualization version GIF version |
Description: An equality deduction for the maps to notation. (Contributed by NM, 12-Sep-2011.) |
Ref | Expression |
---|---|
mpt2eq123dv.1 | ⊢ (𝜑 → 𝐴 = 𝐷) |
mpt2eq123dv.2 | ⊢ (𝜑 → 𝐵 = 𝐸) |
mpt2eq123dv.3 | ⊢ (𝜑 → 𝐶 = 𝐹) |
Ref | Expression |
---|---|
mpt2eq123dv | ⊢ (𝜑 → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑥 ∈ 𝐷, 𝑦 ∈ 𝐸 ↦ 𝐹)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mpt2eq123dv.1 | . 2 ⊢ (𝜑 → 𝐴 = 𝐷) | |
2 | mpt2eq123dv.2 | . . 3 ⊢ (𝜑 → 𝐵 = 𝐸) | |
3 | 2 | adantr 466 | . 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐸) |
4 | mpt2eq123dv.3 | . . 3 ⊢ (𝜑 → 𝐶 = 𝐹) | |
5 | 4 | adantr 466 | . 2 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → 𝐶 = 𝐹) |
6 | 1, 3, 5 | mpt2eq123dva 6864 | 1 ⊢ (𝜑 → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑥 ∈ 𝐷, 𝑦 ∈ 𝐸 ↦ 𝐹)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 382 = wceq 1631 ∈ wcel 2145 ↦ cmpt2 6796 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1870 ax-4 1885 ax-5 1991 ax-6 2057 ax-7 2093 ax-9 2154 ax-10 2174 ax-11 2190 ax-12 2203 ax-ext 2751 |
This theorem depends on definitions: df-bi 197 df-an 383 df-or 829 df-tru 1634 df-ex 1853 df-nf 1858 df-sb 2050 df-clab 2758 df-cleq 2764 df-clel 2767 df-oprab 6798 df-mpt2 6799 |
This theorem is referenced by: mpt2eq123i 6866 mptmpt2opabbrd 7399 el2mpt2csbcl 7401 bropopvvv 7407 bropfvvvv 7409 prdsval 16324 imasval 16380 imasvscaval 16407 homffval 16558 homfeq 16562 comfffval 16566 comffval 16567 comfffval2 16569 comffval2 16570 comfeq 16574 oppcval 16581 monfval 16600 sectffval 16618 invffval 16626 isofn 16643 cofuval 16750 natfval 16814 fucval 16826 fucco 16830 coafval 16922 setcval 16935 setcco 16941 catcval 16954 catcco 16959 estrcval 16972 estrcco 16978 xpcval 17026 xpchomfval 17028 xpccofval 17031 1stfval 17040 2ndfval 17043 prfval 17048 evlfval 17066 evlf2 17067 curfval 17072 hofval 17101 hof2fval 17104 plusffval 17456 grpsubfval 17673 grpsubpropd 17729 mulgfval 17751 mulgpropd 17793 symgval 18007 lsmfval 18261 pj1fval 18315 efgtf 18343 prdsmgp 18819 dvrfval 18893 scaffval 19092 psrval 19578 ipffval 20211 phssip 20221 frlmip 20335 mamufval 20409 mvmulfval 20567 marrepfval 20585 marepvfval 20590 submafval 20604 submaval 20606 madufval 20662 minmar1fval 20671 mat2pmatfval 20749 cpm2mfval 20775 decpmatval0 20790 decpmatval 20791 pmatcollpw3lem 20809 xkoval 21612 xkopt 21680 xpstopnlem1 21834 submtmd 22129 blfvalps 22409 ishtpy 22992 isphtpy 23001 pcofval 23030 rrxip 23398 q1pval 24134 r1pval 24137 taylfval 24334 midf 25890 ismidb 25892 ttgval 25977 wwlksnon 26981 wspthsnon 26982 clwwlknonmpt2 27262 grpodivfval 27729 dipfval 27898 submatres 30213 lmatval 30220 lmatcl 30223 qqhval 30359 sxval 30594 sitmval 30752 cndprobval 30836 mclsval 31799 csbfinxpg 33563 rrnval 33959 ldualset 34935 paddfval 35606 tgrpfset 36554 tgrpset 36555 erngfset 36609 erngset 36610 erngfset-rN 36617 erngset-rN 36618 dvafset 36814 dvaset 36815 dvhfset 36891 dvhset 36892 djaffvalN 36944 djafvalN 36945 djhffval 37207 djhfval 37208 hlhilset 37745 eldiophb 37847 mendval 38280 hoidmvval 41312 ovnhoi 41338 hspval 41344 hspmbllem2 41362 hoimbl 41366 rngcvalALTV 42490 rngccoALTV 42517 funcrngcsetcALT 42528 ringcvalALTV 42536 ringccoALTV 42580 lincop 42726 |
Copyright terms: Public domain | W3C validator |