Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > fvmptg | Structured version Visualization version GIF version |
Description: Value of a function given in maps-to notation. (Contributed by NM, 2-Oct-2007.) (Revised by Mario Carneiro, 31-Aug-2015.) |
Ref | Expression |
---|---|
fvmptg.1 | ⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶) |
fvmptg.2 | ⊢ 𝐹 = (𝑥 ∈ 𝐷 ↦ 𝐵) |
Ref | Expression |
---|---|
fvmptg | ⊢ ((𝐴 ∈ 𝐷 ∧ 𝐶 ∈ 𝑅) → (𝐹‘𝐴) = 𝐶) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqid 2738 | . 2 ⊢ 𝐶 = 𝐶 | |
2 | fvmptg.1 | . . . 4 ⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶) | |
3 | 2 | eqeq2d 2749 | . . 3 ⊢ (𝑥 = 𝐴 → (𝑦 = 𝐵 ↔ 𝑦 = 𝐶)) |
4 | eqeq1 2742 | . . 3 ⊢ (𝑦 = 𝐶 → (𝑦 = 𝐶 ↔ 𝐶 = 𝐶)) | |
5 | moeq 3607 | . . . 4 ⊢ ∃*𝑦 𝑦 = 𝐵 | |
6 | 5 | a1i 11 | . . 3 ⊢ (𝑥 ∈ 𝐷 → ∃*𝑦 𝑦 = 𝐵) |
7 | fvmptg.2 | . . . 4 ⊢ 𝐹 = (𝑥 ∈ 𝐷 ↦ 𝐵) | |
8 | df-mpt 5112 | . . . 4 ⊢ (𝑥 ∈ 𝐷 ↦ 𝐵) = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐷 ∧ 𝑦 = 𝐵)} | |
9 | 7, 8 | eqtri 2761 | . . 3 ⊢ 𝐹 = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐷 ∧ 𝑦 = 𝐵)} |
10 | 3, 4, 6, 9 | fvopab3ig 6772 | . 2 ⊢ ((𝐴 ∈ 𝐷 ∧ 𝐶 ∈ 𝑅) → (𝐶 = 𝐶 → (𝐹‘𝐴) = 𝐶)) |
11 | 1, 10 | mpi 20 | 1 ⊢ ((𝐴 ∈ 𝐷 ∧ 𝐶 ∈ 𝑅) → (𝐹‘𝐴) = 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 399 = wceq 1542 ∈ wcel 2113 ∃*wmo 2538 {copab 5093 ↦ cmpt 5111 ‘cfv 6340 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1916 ax-6 1974 ax-7 2019 ax-8 2115 ax-9 2123 ax-10 2144 ax-11 2161 ax-12 2178 ax-ext 2710 ax-sep 5168 ax-nul 5175 ax-pr 5297 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 847 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1787 df-nf 1791 df-sb 2074 df-mo 2540 df-eu 2570 df-clab 2717 df-cleq 2730 df-clel 2811 df-nfc 2881 df-ral 3058 df-rex 3059 df-v 3400 df-sbc 3683 df-dif 3847 df-un 3849 df-in 3851 df-ss 3861 df-nul 4213 df-if 4416 df-sn 4518 df-pr 4520 df-op 4524 df-uni 4798 df-br 5032 df-opab 5094 df-mpt 5112 df-id 5430 df-xp 5532 df-rel 5533 df-cnv 5534 df-co 5535 df-dm 5536 df-iota 6298 df-fun 6342 df-fv 6348 |
This theorem is referenced by: fvmpti 6775 fvmpt 6776 fvmpt2f 6777 fvtresfn 6778 fvmpts 6779 fvmpt3 6780 fvmptd3 6799 fvmptss2 6801 f1mpt 7031 bropfvvvv 7814 tz7.44-3 8074 pw2f1olem 8671 wdom2d 9118 tz9.12lem3 9292 djurcl 9414 djur 9422 djuun 9429 cardval3 9455 cfval 9748 coftr 9774 fin1a2lem1 9901 fin1a2lem12 9912 axdc2lem 9949 pwcfsdom 10084 tskmval 10340 lsw 14006 swrdswrd 14157 trclfv 14450 relexpsucnnr 14475 dfrtrclrec2 14508 rtrclreclem2 14509 summolem2a 15166 prodmolem2a 15381 divsfval 16924 joinfval 17728 meetfval 17742 symgextfv 18665 symgextfve 18666 pmtrdifwrdel2lem1 18731 efgtf 18967 rrgsupp 20184 uvcvval 20603 ply1sclid 21064 submaval0 21332 m2detleiblem3 21381 m2detleiblem4 21382 maduval 21390 minmar1val0 21399 toponsspwpw 21674 cldval 21775 ntrfval 21776 clsfval 21777 opncldf3 21838 neifval 21851 lpfval 21890 islocfin 22269 kqfval 22475 stdbdxmet 23269 cmetcaulem 24041 bcth3 24084 itg2gt0 24513 ellimc2 24629 coe1termlem 25007 clwlkclwwlkfo 27946 grpoinvfval 28457 grpodivfval 28469 nlfnval 29816 sigaval 31649 measval 31736 measdivcst 31762 measdivcstALTV 31763 probfinmeasbALTV 31966 ptpconn 32766 cvmsval 32799 ex-sategoelel12 32960 bdayval 33492 oldval 33679 imageval 33870 fvimage 33871 tailfval 34199 tailval 34200 curfv 35377 heiborlem4 35592 lkrval 36722 cdleme31fv 38024 docavalN 38757 dochval 38985 mapdval 39262 hvmapval 39394 hvmapvalvalN 39395 hdmap1vallem 39431 hdmapval 39462 hgmapval 39521 mzpval 40118 mzpsubst 40134 pw2f1o2val 40425 refsum2cnlem1 42110 stoweidlem26 43101 stirlinglem8 43156 fourierdlem50 43231 caragenval 43565 fargshiftfv 44417 lincvalsc0 45288 linc0scn0 45290 linc1 45292 lincscm 45297 |
Copyright terms: Public domain | W3C validator |