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

Theorem dffn5 6471
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 6209 . . . . 5 (𝐹 Fn 𝐴 → Rel 𝐹)
2 dfrel4v 5808 . . . . 5 (Rel 𝐹𝐹 = {⟨𝑥, 𝑦⟩ ∣ 𝑥𝐹𝑦})
31, 2sylib 209 . . . 4 (𝐹 Fn 𝐴𝐹 = {⟨𝑥, 𝑦⟩ ∣ 𝑥𝐹𝑦})
4 fnbr 6213 . . . . . . . 8 ((𝐹 Fn 𝐴𝑥𝐹𝑦) → 𝑥𝐴)
54ex 399 . . . . . . 7 (𝐹 Fn 𝐴 → (𝑥𝐹𝑦𝑥𝐴))
65pm4.71rd 554 . . . . . 6 (𝐹 Fn 𝐴 → (𝑥𝐹𝑦 ↔ (𝑥𝐴𝑥𝐹𝑦)))
7 eqcom 2824 . . . . . . . 8 (𝑦 = (𝐹𝑥) ↔ (𝐹𝑥) = 𝑦)
8 fnbrfvb 6465 . . . . . . . 8 ((𝐹 Fn 𝐴𝑥𝐴) → ((𝐹𝑥) = 𝑦𝑥𝐹𝑦))
97, 8syl5bb 274 . . . . . . 7 ((𝐹 Fn 𝐴𝑥𝐴) → (𝑦 = (𝐹𝑥) ↔ 𝑥𝐹𝑦))
109pm5.32da 570 . . . . . 6 (𝐹 Fn 𝐴 → ((𝑥𝐴𝑦 = (𝐹𝑥)) ↔ (𝑥𝐴𝑥𝐹𝑦)))
116, 10bitr4d 273 . . . . 5 (𝐹 Fn 𝐴 → (𝑥𝐹𝑦 ↔ (𝑥𝐴𝑦 = (𝐹𝑥))))
1211opabbidv 4921 . . . 4 (𝐹 Fn 𝐴 → {⟨𝑥, 𝑦⟩ ∣ 𝑥𝐹𝑦} = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 = (𝐹𝑥))})
133, 12eqtrd 2851 . . 3 (𝐹 Fn 𝐴𝐹 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 = (𝐹𝑥))})
14 df-mpt 4935 . . 3 (𝑥𝐴 ↦ (𝐹𝑥)) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 = (𝐹𝑥))}
1513, 14syl6eqr 2869 . 2 (𝐹 Fn 𝐴𝐹 = (𝑥𝐴 ↦ (𝐹𝑥)))
16 fvex 6430 . . . 4 (𝐹𝑥) ∈ V
17 eqid 2817 . . . 4 (𝑥𝐴 ↦ (𝐹𝑥)) = (𝑥𝐴 ↦ (𝐹𝑥))
1816, 17fnmpti 6242 . . 3 (𝑥𝐴 ↦ (𝐹𝑥)) Fn 𝐴
19 fneq1 6199 . . 3 (𝐹 = (𝑥𝐴 ↦ (𝐹𝑥)) → (𝐹 Fn 𝐴 ↔ (𝑥𝐴 ↦ (𝐹𝑥)) Fn 𝐴))
2018, 19mpbiri 249 . 2 (𝐹 = (𝑥𝐴 ↦ (𝐹𝑥)) → 𝐹 Fn 𝐴)
2115, 20impbii 200 1 (𝐹 Fn 𝐴𝐹 = (𝑥𝐴 ↦ (𝐹𝑥)))
Colors of variables: wff setvar class
Syntax hints:  wb 197  wa 384   = wceq 1637  wcel 2157   class class class wbr 4855  {copab 4917  cmpt 4934  Rel wrel 5329   Fn wfn 6105  cfv 6110
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2795  ax-sep 4988  ax-nul 4996  ax-pr 5109
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-mo 2635  df-eu 2642  df-clab 2804  df-cleq 2810  df-clel 2813  df-nfc 2948  df-ral 3112  df-rex 3113  df-rab 3116  df-v 3404  df-sbc 3645  df-dif 3783  df-un 3785  df-in 3787  df-ss 3794  df-nul 4128  df-if 4291  df-sn 4382  df-pr 4384  df-op 4388  df-uni 4642  df-br 4856  df-opab 4918  df-mpt 4935  df-id 5232  df-xp 5330  df-rel 5331  df-cnv 5332  df-co 5333  df-dm 5334  df-iota 6073  df-fun 6112  df-fn 6113  df-fv 6118
This theorem is referenced by:  fnrnfv  6472  feqmptd  6479  dffn5f  6482  eqfnfv  6542  fndmin  6555  fcompt  6632  funiun  6645  resfunexg  6713  eufnfv  6725  nvocnv  6770  fnov  7007  offveqb  7158  caofinvl  7163  oprabco  7504  df1st2  7506  df2nd2  7507  curry1  7512  curry2  7515  resixpfo  8192  pw2f1olem  8312  marypha2lem3  8591  seqof  13100  prmrec  15862  prdsbascl  16367  xpsaddlem  16459  xpsvsca  16463  oppccatid  16602  fuclid  16849  fucrid  16850  curfuncf  17102  yonedainv  17145  yonffthlem  17146  prdsidlem  17546  pws0g  17550  prdsinvlem  17748  gsummptmhm  18560  staffn  19072  prdslmodd  19195  ofco2  20488  1mavmul  20585  cnmpt1st  21705  cnmpt2nd  21706  ptunhmeo  21845  xpsxmetlem  22417  xpsmet  22420  itg2split  23752  pserulm  24412  pserdvlem2  24418  logcn  24629  logblog  24766  emcllem5  24962  gamcvg2lem  25021  crctcshlem4  26963  eucrct2eupth  27440  fcomptf  29807  gsummpt2d  30128  pl1cn  30348  esumpcvgval  30487  esumcvgsum  30497  eulerpartgbij  30781  dstfrvclim1  30886  ptpconn  31559  knoppcnlem8  32828  knoppcnlem11  32831  curfv  33720  ovoliunnfl  33782  voliunnfl  33784  fnopabco  33847  upixp  33854  prdsbnd  33921  prdstotbnd  33922  prdsbnd2  33923  fgraphopab  38306  expgrowthi  39049  expgrowth  39051  uzmptshftfval  39062  dvcosre  40623  fourierdlem56  40875  fourierdlem62  40881  fdmdifeqresdif  42705  offvalfv  42706
  Copyright terms: Public domain W3C validator