![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > dffn5 | Structured version Visualization version GIF version |
Description: Representation of a function in terms of its values. (Contributed by FL, 14-Sep-2013.) (Proof shortened by Mario Carneiro, 31-Aug-2015.) |
Ref | Expression |
---|---|
dffn5 | ⊢ (𝐹 Fn 𝐴 ↔ 𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fnrel 6651 | . . . . 5 ⊢ (𝐹 Fn 𝐴 → Rel 𝐹) | |
2 | dfrel4v 6189 | . . . . 5 ⊢ (Rel 𝐹 ↔ 𝐹 = {〈𝑥, 𝑦〉 ∣ 𝑥𝐹𝑦}) | |
3 | 1, 2 | sylib 217 | . . . 4 ⊢ (𝐹 Fn 𝐴 → 𝐹 = {〈𝑥, 𝑦〉 ∣ 𝑥𝐹𝑦}) |
4 | fnbr 6657 | . . . . . . . 8 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑥𝐹𝑦) → 𝑥 ∈ 𝐴) | |
5 | 4 | ex 412 | . . . . . . 7 ⊢ (𝐹 Fn 𝐴 → (𝑥𝐹𝑦 → 𝑥 ∈ 𝐴)) |
6 | 5 | pm4.71rd 562 | . . . . . 6 ⊢ (𝐹 Fn 𝐴 → (𝑥𝐹𝑦 ↔ (𝑥 ∈ 𝐴 ∧ 𝑥𝐹𝑦))) |
7 | eqcom 2738 | . . . . . . . 8 ⊢ (𝑦 = (𝐹‘𝑥) ↔ (𝐹‘𝑥) = 𝑦) | |
8 | fnbrfvb 6944 | . . . . . . . 8 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑥 ∈ 𝐴) → ((𝐹‘𝑥) = 𝑦 ↔ 𝑥𝐹𝑦)) | |
9 | 7, 8 | bitrid 283 | . . . . . . 7 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝑦 = (𝐹‘𝑥) ↔ 𝑥𝐹𝑦)) |
10 | 9 | pm5.32da 578 | . . . . . 6 ⊢ (𝐹 Fn 𝐴 → ((𝑥 ∈ 𝐴 ∧ 𝑦 = (𝐹‘𝑥)) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥𝐹𝑦))) |
11 | 6, 10 | bitr4d 282 | . . . . 5 ⊢ (𝐹 Fn 𝐴 → (𝑥𝐹𝑦 ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 = (𝐹‘𝑥)))) |
12 | 11 | opabbidv 5214 | . . . 4 ⊢ (𝐹 Fn 𝐴 → {〈𝑥, 𝑦〉 ∣ 𝑥𝐹𝑦} = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = (𝐹‘𝑥))}) |
13 | 3, 12 | eqtrd 2771 | . . 3 ⊢ (𝐹 Fn 𝐴 → 𝐹 = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = (𝐹‘𝑥))}) |
14 | df-mpt 5232 | . . 3 ⊢ (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = (𝐹‘𝑥))} | |
15 | 13, 14 | eqtr4di 2789 | . 2 ⊢ (𝐹 Fn 𝐴 → 𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥))) |
16 | fvex 6904 | . . . 4 ⊢ (𝐹‘𝑥) ∈ V | |
17 | eqid 2731 | . . . 4 ⊢ (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) | |
18 | 16, 17 | fnmpti 6693 | . . 3 ⊢ (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) Fn 𝐴 |
19 | fneq1 6640 | . . 3 ⊢ (𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) → (𝐹 Fn 𝐴 ↔ (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) Fn 𝐴)) | |
20 | 18, 19 | mpbiri 258 | . 2 ⊢ (𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) → 𝐹 Fn 𝐴) |
21 | 15, 20 | impbii 208 | 1 ⊢ (𝐹 Fn 𝐴 ↔ 𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥))) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 205 ∧ wa 395 = wceq 1540 ∈ wcel 2105 class class class wbr 5148 {copab 5210 ↦ cmpt 5231 Rel wrel 5681 Fn wfn 6538 ‘cfv 6543 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1912 ax-6 1970 ax-7 2010 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2153 ax-12 2170 ax-ext 2702 ax-sep 5299 ax-nul 5306 ax-pr 5427 |
This theorem depends on definitions: df-bi 206 df-an 396 df-or 845 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1781 df-nf 1785 df-sb 2067 df-mo 2533 df-eu 2562 df-clab 2709 df-cleq 2723 df-clel 2809 df-nfc 2884 df-ne 2940 df-ral 3061 df-rex 3070 df-rab 3432 df-v 3475 df-dif 3951 df-un 3953 df-in 3955 df-ss 3965 df-nul 4323 df-if 4529 df-sn 4629 df-pr 4631 df-op 4635 df-uni 4909 df-br 5149 df-opab 5211 df-mpt 5232 df-id 5574 df-xp 5682 df-rel 5683 df-cnv 5684 df-co 5685 df-dm 5686 df-iota 6495 df-fun 6545 df-fn 6546 df-fv 6551 |
This theorem is referenced by: fnrnfv 6951 feqmptd 6960 dffn5f 6963 eqfnfv 7032 fndmin 7046 fcompt 7133 funiun 7147 resfunexg 7219 eufnfv 7233 nvocnv 7282 fnov 7543 offveqb 7699 caofinvl 7704 oprabco 8087 df1st2 8089 df2nd2 8090 curry1 8095 curry2 8098 resixpfo 8936 pw2f1olem 9082 marypha2lem3 9438 seqof 14032 prmrec 16862 prdsbascl 17436 xpsaddlem 17526 xpsvsca 17530 oppccatid 17672 fuclid 17929 fucrid 17930 curfuncf 18201 yonedainv 18244 yonffthlem 18245 prdsidlem 18697 pws0g 18701 prdsinvlem 18975 gsummptmhm 19856 staffn 20688 prdslmodd 20812 ofco2 22272 1mavmul 22369 cnmpt1st 23491 cnmpt2nd 23492 ptunhmeo 23631 xpsxmetlem 24204 xpsmet 24207 itg2split 25598 pserulm 26272 pserdvlem2 26279 logcn 26494 logblog 26637 emcllem5 26844 gamcvg2lem 26903 crctcshlem4 29506 eucrct2eupth 29930 fcomptf 32315 gsummpt2d 32636 pl1cn 33398 esumpcvgval 33539 esumcvgsum 33549 eulerpartgbij 33834 dstfrvclim1 33939 ptpconn 34687 knoppcnlem8 35839 knoppcnlem11 35842 ctbssinf 36750 curfv 36931 ovoliunnfl 36993 voliunnfl 36995 fnopabco 37054 upixp 37060 prdsbnd 37124 prdstotbnd 37125 prdsbnd2 37126 sticksstones12a 41439 sticksstones12 41440 sticksstones19 41447 fgraphopab 42414 rp-tfslim 42565 expgrowthi 43554 expgrowth 43556 uzmptshftfval 43567 dvcosre 45086 fourierdlem56 45336 fourierdlem62 45342 fundcmpsurbijinjpreimafv 46533 fundcmpsurinjimaid 46537 fdmdifeqresdif 47179 offvalfv 47180 |
Copyright terms: Public domain | W3C validator |