Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > fvmptg | 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 2117 | . 2 ⊢ 𝐶 = 𝐶 | |
2 | fvmptg.1 | . . . 4 ⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶) | |
3 | 2 | eqeq2d 2129 | . . 3 ⊢ (𝑥 = 𝐴 → (𝑦 = 𝐵 ↔ 𝑦 = 𝐶)) |
4 | eqeq1 2124 | . . 3 ⊢ (𝑦 = 𝐶 → (𝑦 = 𝐶 ↔ 𝐶 = 𝐶)) | |
5 | moeq 2832 | . . . 4 ⊢ ∃*𝑦 𝑦 = 𝐵 | |
6 | 5 | a1i 9 | . . 3 ⊢ (𝑥 ∈ 𝐷 → ∃*𝑦 𝑦 = 𝐵) |
7 | fvmptg.2 | . . . 4 ⊢ 𝐹 = (𝑥 ∈ 𝐷 ↦ 𝐵) | |
8 | df-mpt 3961 | . . . 4 ⊢ (𝑥 ∈ 𝐷 ↦ 𝐵) = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐷 ∧ 𝑦 = 𝐵)} | |
9 | 7, 8 | eqtri 2138 | . . 3 ⊢ 𝐹 = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐷 ∧ 𝑦 = 𝐵)} |
10 | 3, 4, 6, 9 | fvopab3ig 5463 | . 2 ⊢ ((𝐴 ∈ 𝐷 ∧ 𝐶 ∈ 𝑅) → (𝐶 = 𝐶 → (𝐹‘𝐴) = 𝐶)) |
11 | 1, 10 | mpi 15 | 1 ⊢ ((𝐴 ∈ 𝐷 ∧ 𝐶 ∈ 𝑅) → (𝐹‘𝐴) = 𝐶) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 = wceq 1316 ∈ wcel 1465 ∃*wmo 1978 {copab 3958 ↦ cmpt 3959 ‘cfv 5093 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-io 683 ax-5 1408 ax-7 1409 ax-gen 1410 ax-ie1 1454 ax-ie2 1455 ax-8 1467 ax-10 1468 ax-11 1469 ax-i12 1470 ax-bndl 1471 ax-4 1472 ax-14 1477 ax-17 1491 ax-i9 1495 ax-ial 1499 ax-i5r 1500 ax-ext 2099 ax-sep 4016 ax-pow 4068 ax-pr 4101 |
This theorem depends on definitions: df-bi 116 df-3an 949 df-tru 1319 df-nf 1422 df-sb 1721 df-eu 1980 df-mo 1981 df-clab 2104 df-cleq 2110 df-clel 2113 df-nfc 2247 df-ral 2398 df-rex 2399 df-v 2662 df-sbc 2883 df-un 3045 df-in 3047 df-ss 3054 df-pw 3482 df-sn 3503 df-pr 3504 df-op 3506 df-uni 3707 df-br 3900 df-opab 3960 df-mpt 3961 df-id 4185 df-xp 4515 df-rel 4516 df-cnv 4517 df-co 4518 df-dm 4519 df-iota 5058 df-fun 5095 df-fv 5101 |
This theorem is referenced by: fvmpt 5466 fvmpts 5467 fvmpt3 5468 fvmpt2 5472 f1mpt 5640 caofinvl 5972 1stvalg 6008 2ndvalg 6009 brtpos2 6116 rdgon 6251 frec0g 6262 freccllem 6267 frecfcllem 6269 frecsuclem 6271 sucinc 6309 sucinc2 6310 omcl 6325 oeicl 6326 oav2 6327 omv2 6329 fvdiagfn 6555 djulclr 6902 djurclr 6903 djulcl 6904 djurcl 6905 djulclb 6908 omp1eomlem 6947 ctmlemr 6961 nnnninf 6991 cardval3ex 7009 ceilqval 10047 frec2uzzd 10141 frec2uzsucd 10142 monoord2 10218 iseqf1olemqval 10228 iseqf1olemqk 10235 seq3f1olemqsum 10241 seq3f1oleml 10244 seq3f1o 10245 seq3distr 10254 ser3le 10259 hashinfom 10492 hashennn 10494 cjval 10585 reval 10589 imval 10590 cvg1nlemcau 10724 cvg1nlemres 10725 absval 10741 resqrexlemglsq 10762 resqrexlemga 10763 climmpt 11037 climle 11071 climcvg1nlem 11086 summodclem3 11117 summodclem2a 11118 zsumdc 11121 fsum3 11124 fsumcl2lem 11135 sumsnf 11146 isumadd 11168 fsumrev 11180 fsumshft 11181 fsummulc2 11185 iserabs 11212 isumlessdc 11233 divcnv 11234 trireciplem 11237 trirecip 11238 expcnvap0 11239 expcnvre 11240 expcnv 11241 explecnv 11242 geolim 11248 geolim2 11249 geo2lim 11253 geoisum 11254 geoisumr 11255 geoisum1 11256 geoisum1c 11257 cvgratz 11269 mertenslem2 11273 mertensabs 11274 eftvalcn 11290 efval 11294 efcvgfsum 11300 ege2le3 11304 efcj 11306 eftlub 11323 efgt1p2 11328 eflegeo 11335 sinval 11336 cosval 11337 tanvalap 11342 eirraplem 11410 phival 11816 crth 11827 phimullem 11828 ennnfonelemj0 11841 ennnfonelem0 11845 strnfvnd 11906 topnvalg 12059 toponsspwpwg 12116 tgval 12145 cldval 12195 ntrfval 12196 clsfval 12197 neifval 12236 neival 12239 ismet 12440 isxmet 12441 divcnap 12651 mulc1cncf 12672 djucllem 12934 nnsf 13126 peano3nninf 13128 nninfalllemn 13129 nninfself 13136 nninfsellemeqinf 13139 |
Copyright terms: Public domain | W3C validator |