![]() |
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 2733 | . 2 ⊢ 𝐶 = 𝐶 | |
2 | fvmptg.1 | . . . 4 ⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶) | |
3 | 2 | eqeq2d 2744 | . . 3 ⊢ (𝑥 = 𝐴 → (𝑦 = 𝐵 ↔ 𝑦 = 𝐶)) |
4 | eqeq1 2737 | . . 3 ⊢ (𝑦 = 𝐶 → (𝑦 = 𝐶 ↔ 𝐶 = 𝐶)) | |
5 | moeq 3704 | . . . 4 ⊢ ∃*𝑦 𝑦 = 𝐵 | |
6 | 5 | a1i 11 | . . 3 ⊢ (𝑥 ∈ 𝐷 → ∃*𝑦 𝑦 = 𝐵) |
7 | fvmptg.2 | . . . 4 ⊢ 𝐹 = (𝑥 ∈ 𝐷 ↦ 𝐵) | |
8 | df-mpt 5233 | . . . 4 ⊢ (𝑥 ∈ 𝐷 ↦ 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐷 ∧ 𝑦 = 𝐵)} | |
9 | 7, 8 | eqtri 2761 | . . 3 ⊢ 𝐹 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐷 ∧ 𝑦 = 𝐵)} |
10 | 3, 4, 6, 9 | fvopab3ig 6995 | . 2 ⊢ ((𝐴 ∈ 𝐷 ∧ 𝐶 ∈ 𝑅) → (𝐶 = 𝐶 → (𝐹‘𝐴) = 𝐶)) |
11 | 1, 10 | mpi 20 | 1 ⊢ ((𝐴 ∈ 𝐷 ∧ 𝐶 ∈ 𝑅) → (𝐹‘𝐴) = 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 397 = wceq 1542 ∈ wcel 2107 ∃*wmo 2533 {copab 5211 ↦ cmpt 5232 ‘cfv 6544 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-10 2138 ax-11 2155 ax-12 2172 ax-ext 2704 ax-sep 5300 ax-nul 5307 ax-pr 5428 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-nf 1787 df-sb 2069 df-mo 2535 df-eu 2564 df-clab 2711 df-cleq 2725 df-clel 2811 df-nfc 2886 df-ral 3063 df-rex 3072 df-rab 3434 df-v 3477 df-dif 3952 df-un 3954 df-in 3956 df-ss 3966 df-nul 4324 df-if 4530 df-sn 4630 df-pr 4632 df-op 4636 df-uni 4910 df-br 5150 df-opab 5212 df-mpt 5233 df-id 5575 df-xp 5683 df-rel 5684 df-cnv 5685 df-co 5686 df-dm 5687 df-iota 6496 df-fun 6546 df-fv 6552 |
This theorem is referenced by: fvmpti 6998 fvmpt 6999 fvmpt2f 7000 fvtresfn 7001 fvmpts 7002 fvmpt3 7003 fvmptd3 7022 fvmptss2 7024 f1mpt 7260 bropfvvvv 8078 tz7.44-3 8408 pw2f1olem 9076 wdom2d 9575 tz9.12lem3 9784 djurcl 9906 djur 9914 djuun 9921 cardval3 9947 cfval 10242 coftr 10268 fin1a2lem1 10395 fin1a2lem12 10406 axdc2lem 10443 pwcfsdom 10578 tskmval 10834 lsw 14514 swrdswrd 14655 trclfv 14947 relexpsucnnr 14972 dfrtrclrec2 15005 rtrclreclem2 15006 summolem2a 15661 prodmolem2a 15878 divsfval 17493 joinfval 18326 meetfval 18340 symgextfv 19286 symgextfve 19287 pmtrdifwrdel2lem1 19352 efgtf 19590 rrgsupp 20907 uvcvval 21341 ply1sclid 21810 submaval0 22082 m2detleiblem3 22131 m2detleiblem4 22132 maduval 22140 minmar1val0 22149 toponsspwpw 22424 cldval 22527 ntrfval 22528 clsfval 22529 opncldf3 22590 neifval 22603 lpfval 22642 islocfin 23021 kqfval 23227 stdbdxmet 24024 cmetcaulem 24805 bcth3 24848 itg2gt0 25278 ellimc2 25394 coe1termlem 25772 bdayval 27151 oldval 27349 clwlkclwwlkfo 29262 grpoinvfval 29775 grpodivfval 29787 nlfnval 31134 sigaval 33109 measval 33196 measdivcst 33222 measdivcstALTV 33223 probfinmeasbALTV 33428 ptpconn 34224 cvmsval 34257 ex-sategoelel12 34418 imageval 34902 fvimage 34903 tailfval 35257 tailval 35258 curfv 36468 heiborlem4 36682 lkrval 37958 cdleme31fv 39261 docavalN 39994 dochval 40222 mapdval 40499 hvmapval 40631 hvmapvalvalN 40632 hdmap1vallem 40668 hdmapval 40699 hgmapval 40758 mzpval 41470 mzpsubst 41486 pw2f1o2val 41778 refsum2cnlem1 43721 stoweidlem26 44742 stirlinglem8 44797 fourierdlem50 44872 caragenval 45209 fargshiftfv 46107 lincvalsc0 47102 linc0scn0 47104 linc1 47106 lincscm 47111 |
Copyright terms: Public domain | W3C validator |