![]() |
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 474 | . 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 = 𝐸) |
4 | mpt2eq123dv.3 | . . 3 ⊢ (𝜑 → 𝐶 = 𝐹) | |
5 | 4 | adantr 474 | . 2 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → 𝐶 = 𝐹) |
6 | 1, 3, 5 | mpt2eq123dva 6995 | 1 ⊢ (𝜑 → (𝑥 ∈ 𝐴, 𝑦 ∈ 𝐵 ↦ 𝐶) = (𝑥 ∈ 𝐷, 𝑦 ∈ 𝐸 ↦ 𝐹)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 386 = wceq 1601 ∈ wcel 2107 ↦ cmpt2 6926 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1839 ax-4 1853 ax-5 1953 ax-6 2021 ax-7 2055 ax-9 2116 ax-12 2163 ax-ext 2754 |
This theorem depends on definitions: df-bi 199 df-an 387 df-ex 1824 df-nf 1828 df-sb 2012 df-clab 2764 df-cleq 2770 df-clel 2774 df-oprab 6928 df-mpt2 6929 |
This theorem is referenced by: mpt2eq123i 6997 mptmpt2opabbrd 7530 el2mpt2csbcl 7532 bropopvvv 7538 bropfvvvv 7540 prdsval 16505 imasval 16561 imasvscaval 16588 homffval 16739 homfeq 16743 comfffval 16747 comffval 16748 comfffval2 16750 comffval2 16751 comfeq 16755 oppcval 16762 monfval 16781 sectffval 16799 invffval 16807 isofn 16824 cofuval 16931 natfval 16995 fucval 17007 fucco 17011 coafval 17103 setcval 17116 setcco 17122 catcval 17135 catcco 17140 estrcval 17153 estrcco 17159 xpcval 17207 xpchomfval 17209 xpccofval 17212 1stfval 17221 2ndfval 17224 prfval 17229 evlfval 17247 evlf2 17248 curfval 17253 hofval 17282 hof2fval 17285 plusffval 17637 grpsubfval 17855 grpsubpropd 17911 mulgfval 17933 mulgpropd 17972 symgval 18186 lsmfval 18441 pj1fval 18495 efgtf 18523 prdsmgp 19001 dvrfval 19075 scaffval 19277 psrval 19763 ipffval 20395 phssip 20405 frlmip 20525 mamufval 20599 mvmulfval 20757 marrepfval 20775 marepvfval 20780 submafval 20794 submaval 20796 madufval 20852 minmar1fval 20861 mat2pmatfval 20939 cpm2mfval 20965 decpmatval0 20980 decpmatval 20981 pmatcollpw3lem 20999 xkoval 21803 xkopt 21871 xpstopnlem1 22025 submtmd 22320 blfvalps 22600 ishtpy 23183 isphtpy 23192 pcofval 23221 rrxip 23600 q1pval 24354 r1pval 24357 taylfval 24554 midf 26128 ismidb 26130 ttgval 26228 wwlksnon 27204 wspthsnon 27205 clwwlknonmpt2 27495 grpodivfval 27965 dipfval 28133 submatres 30474 lmatval 30481 lmatcl 30484 qqhval 30620 sxval 30855 sitmval 31013 cndprobval 31098 mclsval 32063 csbfinxpg 33823 rrnval 34255 ldualset 35284 paddfval 35956 tgrpfset 36903 tgrpset 36904 erngfset 36958 erngset 36959 erngfset-rN 36966 erngset-rN 36967 dvafset 37163 dvaset 37164 dvhfset 37239 dvhset 37240 djaffvalN 37292 djafvalN 37293 djhffval 37555 djhfval 37556 hlhilset 38093 eldiophb 38290 mendval 38722 hoidmvval 41728 ovnhoi 41754 hspval 41760 hspmbllem2 41778 hoimbl 41782 rngcvalALTV 42986 rngccoALTV 43013 funcrngcsetcALT 43024 ringcvalALTV 43032 ringccoALTV 43076 lincop 43222 lines 43477 rrxlines 43479 spheres 43492 |
Copyright terms: Public domain | W3C validator |