![]() |
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 2798 | . 2 ⊢ 𝐶 = 𝐶 | |
2 | fvmptg.1 | . . . 4 ⊢ (𝑥 = 𝐴 → 𝐵 = 𝐶) | |
3 | 2 | eqeq2d 2809 | . . 3 ⊢ (𝑥 = 𝐴 → (𝑦 = 𝐵 ↔ 𝑦 = 𝐶)) |
4 | eqeq1 2802 | . . 3 ⊢ (𝑦 = 𝐶 → (𝑦 = 𝐶 ↔ 𝐶 = 𝐶)) | |
5 | moeq 3646 | . . . 4 ⊢ ∃*𝑦 𝑦 = 𝐵 | |
6 | 5 | a1i 11 | . . 3 ⊢ (𝑥 ∈ 𝐷 → ∃*𝑦 𝑦 = 𝐵) |
7 | fvmptg.2 | . . . 4 ⊢ 𝐹 = (𝑥 ∈ 𝐷 ↦ 𝐵) | |
8 | df-mpt 5111 | . . . 4 ⊢ (𝑥 ∈ 𝐷 ↦ 𝐵) = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐷 ∧ 𝑦 = 𝐵)} | |
9 | 7, 8 | eqtri 2821 | . . 3 ⊢ 𝐹 = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐷 ∧ 𝑦 = 𝐵)} |
10 | 3, 4, 6, 9 | fvopab3ig 6741 | . 2 ⊢ ((𝐴 ∈ 𝐷 ∧ 𝐶 ∈ 𝑅) → (𝐶 = 𝐶 → (𝐹‘𝐴) = 𝐶)) |
11 | 1, 10 | mpi 20 | 1 ⊢ ((𝐴 ∈ 𝐷 ∧ 𝐶 ∈ 𝑅) → (𝐹‘𝐴) = 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 399 = wceq 1538 ∈ wcel 2111 ∃*wmo 2596 {copab 5092 ↦ cmpt 5110 ‘cfv 6324 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-10 2142 ax-11 2158 ax-12 2175 ax-ext 2770 ax-sep 5167 ax-nul 5174 ax-pr 5295 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 845 df-3an 1086 df-tru 1541 df-ex 1782 df-nf 1786 df-sb 2070 df-mo 2598 df-eu 2629 df-clab 2777 df-cleq 2791 df-clel 2870 df-nfc 2938 df-ral 3111 df-rex 3112 df-v 3443 df-sbc 3721 df-dif 3884 df-un 3886 df-in 3888 df-ss 3898 df-nul 4244 df-if 4426 df-sn 4526 df-pr 4528 df-op 4532 df-uni 4801 df-br 5031 df-opab 5093 df-mpt 5111 df-id 5425 df-xp 5525 df-rel 5526 df-cnv 5527 df-co 5528 df-dm 5529 df-iota 6283 df-fun 6326 df-fv 6332 |
This theorem is referenced by: fvmpti 6744 fvmpt 6745 fvmpt2f 6746 fvtresfn 6747 fvmpts 6748 fvmpt3 6749 fvmptd3 6768 fvmptss2 6770 f1mpt 6997 bropfvvvv 7770 tz7.44-3 8027 pw2f1olem 8604 wdom2d 9028 tz9.12lem3 9202 djurcl 9324 djur 9332 djuun 9339 cardval3 9365 cfval 9658 coftr 9684 fin1a2lem1 9811 fin1a2lem12 9822 axdc2lem 9859 pwcfsdom 9994 tskmval 10250 lsw 13907 swrdswrd 14058 trclfv 14351 relexpsucnnr 14376 dfrtrclrec2 14409 rtrclreclem2 14410 summolem2a 15064 prodmolem2a 15280 divsfval 16812 joinfval 17603 meetfval 17617 symgextfv 18538 symgextfve 18539 pmtrdifwrdel2lem1 18604 efgtf 18840 rrgsupp 20057 uvcvval 20475 ply1sclid 20917 submaval0 21185 m2detleiblem3 21234 m2detleiblem4 21235 maduval 21243 minmar1val0 21252 toponsspwpw 21527 cldval 21628 ntrfval 21629 clsfval 21630 opncldf3 21691 neifval 21704 lpfval 21743 islocfin 22122 kqfval 22328 stdbdxmet 23122 cmetcaulem 23892 bcth3 23935 itg2gt0 24364 ellimc2 24480 coe1termlem 24855 clwlkclwwlkfo 27794 grpoinvfval 28305 grpodivfval 28317 nlfnval 29664 sigaval 31480 measval 31567 measdivcst 31593 measdivcstALTV 31594 probfinmeasbALTV 31797 ptpconn 32593 cvmsval 32626 ex-sategoelel12 32787 bdayval 33268 imageval 33504 fvimage 33505 tailfval 33833 tailval 33834 curfv 35037 heiborlem4 35252 lkrval 36384 cdleme31fv 37686 docavalN 38419 dochval 38647 mapdval 38924 hvmapval 39056 hvmapvalvalN 39057 hdmap1vallem 39093 hdmapval 39124 hgmapval 39183 mzpval 39673 mzpsubst 39689 pw2f1o2val 39980 refsum2cnlem1 41666 stoweidlem26 42668 stirlinglem8 42723 fourierdlem50 42798 caragenval 43132 fargshiftfv 43956 lincvalsc0 44830 linc0scn0 44832 linc1 44834 lincscm 44839 |
Copyright terms: Public domain | W3C validator |