Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  dffn5 Structured version   Visualization version   GIF version

Theorem dffn5 6703
 Description: Representation of a function in terms of its values. (Contributed by FL, 14-Sep-2013.) (Proof shortened by Mario Carneiro, 31-Aug-2015.)
Assertion
Ref Expression
dffn5 (𝐹 Fn 𝐴𝐹 = (𝑥𝐴 ↦ (𝐹𝑥)))
Distinct variable groups:   𝑥,𝐴   𝑥,𝐹

Proof of Theorem dffn5
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 fnrel 6428 . . . . 5 (𝐹 Fn 𝐴 → Rel 𝐹)
2 dfrel4v 6018 . . . . 5 (Rel 𝐹𝐹 = {⟨𝑥, 𝑦⟩ ∣ 𝑥𝐹𝑦})
31, 2sylib 221 . . . 4 (𝐹 Fn 𝐴𝐹 = {⟨𝑥, 𝑦⟩ ∣ 𝑥𝐹𝑦})
4 fnbr 6434 . . . . . . . 8 ((𝐹 Fn 𝐴𝑥𝐹𝑦) → 𝑥𝐴)
54ex 416 . . . . . . 7 (𝐹 Fn 𝐴 → (𝑥𝐹𝑦𝑥𝐴))
65pm4.71rd 566 . . . . . 6 (𝐹 Fn 𝐴 → (𝑥𝐹𝑦 ↔ (𝑥𝐴𝑥𝐹𝑦)))
7 eqcom 2808 . . . . . . . 8 (𝑦 = (𝐹𝑥) ↔ (𝐹𝑥) = 𝑦)
8 fnbrfvb 6697 . . . . . . . 8 ((𝐹 Fn 𝐴𝑥𝐴) → ((𝐹𝑥) = 𝑦𝑥𝐹𝑦))
97, 8syl5bb 286 . . . . . . 7 ((𝐹 Fn 𝐴𝑥𝐴) → (𝑦 = (𝐹𝑥) ↔ 𝑥𝐹𝑦))
109pm5.32da 582 . . . . . 6 (𝐹 Fn 𝐴 → ((𝑥𝐴𝑦 = (𝐹𝑥)) ↔ (𝑥𝐴𝑥𝐹𝑦)))
116, 10bitr4d 285 . . . . 5 (𝐹 Fn 𝐴 → (𝑥𝐹𝑦 ↔ (𝑥𝐴𝑦 = (𝐹𝑥))))
1211opabbidv 5099 . . . 4 (𝐹 Fn 𝐴 → {⟨𝑥, 𝑦⟩ ∣ 𝑥𝐹𝑦} = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 = (𝐹𝑥))})
133, 12eqtrd 2836 . . 3 (𝐹 Fn 𝐴𝐹 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 = (𝐹𝑥))})
14 df-mpt 5114 . . 3 (𝑥𝐴 ↦ (𝐹𝑥)) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 = (𝐹𝑥))}
1513, 14eqtr4di 2854 . 2 (𝐹 Fn 𝐴𝐹 = (𝑥𝐴 ↦ (𝐹𝑥)))
16 fvex 6662 . . . 4 (𝐹𝑥) ∈ V
17 eqid 2801 . . . 4 (𝑥𝐴 ↦ (𝐹𝑥)) = (𝑥𝐴 ↦ (𝐹𝑥))
1816, 17fnmpti 6467 . . 3 (𝑥𝐴 ↦ (𝐹𝑥)) Fn 𝐴
19 fneq1 6418 . . 3 (𝐹 = (𝑥𝐴 ↦ (𝐹𝑥)) → (𝐹 Fn 𝐴 ↔ (𝑥𝐴 ↦ (𝐹𝑥)) Fn 𝐴))
2018, 19mpbiri 261 . 2 (𝐹 = (𝑥𝐴 ↦ (𝐹𝑥)) → 𝐹 Fn 𝐴)
2115, 20impbii 212 1 (𝐹 Fn 𝐴𝐹 = (𝑥𝐴 ↦ (𝐹𝑥)))
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 209   ∧ wa 399   = wceq 1538   ∈ wcel 2112   class class class wbr 5033  {copab 5095   ↦ cmpt 5113  Rel wrel 5528   Fn wfn 6323  ‘cfv 6328 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 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773  ax-sep 5170  ax-nul 5177  ax-pr 5298 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 2601  df-eu 2632  df-clab 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-ral 3114  df-rex 3115  df-v 3446  df-sbc 3724  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-nul 4247  df-if 4429  df-sn 4529  df-pr 4531  df-op 4535  df-uni 4804  df-br 5034  df-opab 5096  df-mpt 5114  df-id 5428  df-xp 5529  df-rel 5530  df-cnv 5531  df-co 5532  df-dm 5533  df-iota 6287  df-fun 6330  df-fn 6331  df-fv 6336 This theorem is referenced by:  fnrnfv  6704  feqmptd  6712  dffn5f  6715  eqfnfv  6783  fndmin  6796  fcompt  6876  funiun  6890  resfunexg  6959  eufnfv  6973  nvocnv  7020  fnov  7265  offveqb  7415  caofinvl  7420  oprabco  7778  df1st2  7780  df2nd2  7781  curry1  7786  curry2  7789  resixpfo  8487  pw2f1olem  8608  marypha2lem3  8889  seqof  13427  prmrec  16251  prdsbascl  16751  xpsaddlem  16841  xpsvsca  16845  oppccatid  16984  fuclid  17231  fucrid  17232  curfuncf  17483  yonedainv  17526  yonffthlem  17527  prdsidlem  17938  pws0g  17942  prdsinvlem  18203  gsummptmhm  19056  staffn  19616  prdslmodd  19737  ofco2  21059  1mavmul  21156  cnmpt1st  22276  cnmpt2nd  22277  ptunhmeo  22416  xpsxmetlem  22989  xpsmet  22992  itg2split  24356  pserulm  25020  pserdvlem2  25026  logcn  25241  logblog  25381  emcllem5  25588  gamcvg2lem  25647  crctcshlem4  27609  eucrct2eupth  28033  fcomptf  30424  gsummpt2d  30737  pl1cn  31306  esumpcvgval  31445  esumcvgsum  31455  eulerpartgbij  31738  dstfrvclim1  31843  ptpconn  32588  knoppcnlem8  33947  knoppcnlem11  33950  ctbssinf  34818  curfv  35030  ovoliunnfl  35092  voliunnfl  35094  fnopabco  35154  upixp  35160  prdsbnd  35224  prdstotbnd  35225  prdsbnd2  35226  fgraphopab  40141  expgrowthi  41024  expgrowth  41026  uzmptshftfval  41037  dvcosre  42541  fourierdlem56  42791  fourierdlem62  42797  fundcmpsurbijinjpreimafv  43911  fundcmpsurinjimaid  43915  fdmdifeqresdif  44730  offvalfv  44731
 Copyright terms: Public domain W3C validator