![]() |
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 2187 | . 2 ⊢ 𝐶 = 𝐶 | |
2 | fvmptg.1 | . . . 4 ⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶) | |
3 | 2 | eqeq2d 2199 | . . 3 ⊢ (𝑥 = 𝐴 → (𝑦 = 𝐵 ↔ 𝑦 = 𝐶)) |
4 | eqeq1 2194 | . . 3 ⊢ (𝑦 = 𝐶 → (𝑦 = 𝐶 ↔ 𝐶 = 𝐶)) | |
5 | moeq 2924 | . . . 4 ⊢ ∃*𝑦 𝑦 = 𝐵 | |
6 | 5 | a1i 9 | . . 3 ⊢ (𝑥 ∈ 𝐷 → ∃*𝑦 𝑦 = 𝐵) |
7 | fvmptg.2 | . . . 4 ⊢ 𝐹 = (𝑥 ∈ 𝐷 ↦ 𝐵) | |
8 | df-mpt 4078 | . . . 4 ⊢ (𝑥 ∈ 𝐷 ↦ 𝐵) = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐷 ∧ 𝑦 = 𝐵)} | |
9 | 7, 8 | eqtri 2208 | . . 3 ⊢ 𝐹 = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐷 ∧ 𝑦 = 𝐵)} |
10 | 3, 4, 6, 9 | fvopab3ig 5603 | . 2 ⊢ ((𝐴 ∈ 𝐷 ∧ 𝐶 ∈ 𝑅) → (𝐶 = 𝐶 → (𝐹‘𝐴) = 𝐶)) |
11 | 1, 10 | mpi 15 | 1 ⊢ ((𝐴 ∈ 𝐷 ∧ 𝐶 ∈ 𝑅) → (𝐹‘𝐴) = 𝐶) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 104 = wceq 1363 ∃*wmo 2037 ∈ wcel 2158 {copab 4075 ↦ cmpt 4076 ‘cfv 5228 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-io 710 ax-5 1457 ax-7 1458 ax-gen 1459 ax-ie1 1503 ax-ie2 1504 ax-8 1514 ax-10 1515 ax-11 1516 ax-i12 1517 ax-bndl 1519 ax-4 1520 ax-17 1536 ax-i9 1540 ax-ial 1544 ax-i5r 1545 ax-14 2161 ax-ext 2169 ax-sep 4133 ax-pow 4186 ax-pr 4221 |
This theorem depends on definitions: df-bi 117 df-3an 981 df-tru 1366 df-nf 1471 df-sb 1773 df-eu 2039 df-mo 2040 df-clab 2174 df-cleq 2180 df-clel 2183 df-nfc 2318 df-ral 2470 df-rex 2471 df-v 2751 df-sbc 2975 df-un 3145 df-in 3147 df-ss 3154 df-pw 3589 df-sn 3610 df-pr 3611 df-op 3613 df-uni 3822 df-br 4016 df-opab 4077 df-mpt 4078 df-id 4305 df-xp 4644 df-rel 4645 df-cnv 4646 df-co 4647 df-dm 4648 df-iota 5190 df-fun 5230 df-fv 5236 |
This theorem is referenced by: fvmpt 5606 fvmpts 5607 fvmpt3 5608 fvmpt2 5612 f1mpt 5785 caofinvl 6119 1stvalg 6157 2ndvalg 6158 brtpos2 6266 rdgon 6401 frec0g 6412 freccllem 6417 frecfcllem 6419 frecsuclem 6421 sucinc 6460 sucinc2 6461 omcl 6476 oeicl 6477 oav2 6478 omv2 6480 fvdiagfn 6707 djulclr 7062 djurclr 7063 djulcl 7064 djurcl 7065 djulclb 7068 omp1eomlem 7107 ctmlemr 7121 nnnninf 7138 nnnninfeq 7140 cardval3ex 7198 ceilqval 10320 frec2uzzd 10414 frec2uzsucd 10415 monoord2 10491 iseqf1olemqval 10501 iseqf1olemqk 10508 seq3f1olemqsum 10514 seq3f1oleml 10517 seq3f1o 10518 seq3distr 10527 ser3le 10532 hashinfom 10772 hashennn 10774 cjval 10868 reval 10872 imval 10873 cvg1nlemcau 11007 cvg1nlemres 11008 absval 11024 resqrexlemglsq 11045 resqrexlemga 11046 climmpt 11322 climle 11356 climcvg1nlem 11371 summodclem3 11402 summodclem2a 11403 zsumdc 11406 fsum3 11409 fsumcl2lem 11420 sumsnf 11431 isumadd 11453 fsumrev 11465 fsumshft 11466 fsummulc2 11470 iserabs 11497 isumlessdc 11518 divcnv 11519 trireciplem 11522 trirecip 11523 expcnvap0 11524 expcnvre 11525 expcnv 11526 explecnv 11527 geolim 11533 geolim2 11534 geo2lim 11538 geoisum 11539 geoisumr 11540 geoisum1 11541 geoisum1c 11542 cvgratz 11554 mertenslem2 11558 mertensabs 11559 fprodmul 11613 eftvalcn 11679 efval 11683 efcvgfsum 11689 ege2le3 11693 efcj 11695 eftlub 11712 efgt1p2 11717 eflegeo 11723 sinval 11724 cosval 11725 tanvalap 11730 eirraplem 11798 phival 12227 crth 12238 phimullem 12239 ennnfonelemj0 12416 ennnfonelem0 12420 strnfvnd 12496 topnvalg 12718 tgval 12729 toponsspwpwg 13875 cldval 13952 ntrfval 13953 clsfval 13954 neifval 13993 neival 13996 ismet 14197 isxmet 14198 divcnap 14408 mulc1cncf 14429 djucllem 14905 nnsf 15108 peano3nninf 15110 nninfself 15116 nninfsellemeqinf 15119 dceqnconst 15162 dcapnconst 15163 |
Copyright terms: Public domain | W3C validator |