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

Theorem dffn5 6404
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 6150 . . . . 5 (𝐹 Fn 𝐴 → Rel 𝐹)
2 dfrel4v 5742 . . . . 5 (Rel 𝐹𝐹 = {⟨𝑥, 𝑦⟩ ∣ 𝑥𝐹𝑦})
31, 2sylib 208 . . . 4 (𝐹 Fn 𝐴𝐹 = {⟨𝑥, 𝑦⟩ ∣ 𝑥𝐹𝑦})
4 fnbr 6154 . . . . . . . 8 ((𝐹 Fn 𝐴𝑥𝐹𝑦) → 𝑥𝐴)
54ex 449 . . . . . . 7 (𝐹 Fn 𝐴 → (𝑥𝐹𝑦𝑥𝐴))
65pm4.71rd 670 . . . . . 6 (𝐹 Fn 𝐴 → (𝑥𝐹𝑦 ↔ (𝑥𝐴𝑥𝐹𝑦)))
7 eqcom 2767 . . . . . . . 8 (𝑦 = (𝐹𝑥) ↔ (𝐹𝑥) = 𝑦)
8 fnbrfvb 6398 . . . . . . . 8 ((𝐹 Fn 𝐴𝑥𝐴) → ((𝐹𝑥) = 𝑦𝑥𝐹𝑦))
97, 8syl5bb 272 . . . . . . 7 ((𝐹 Fn 𝐴𝑥𝐴) → (𝑦 = (𝐹𝑥) ↔ 𝑥𝐹𝑦))
109pm5.32da 676 . . . . . 6 (𝐹 Fn 𝐴 → ((𝑥𝐴𝑦 = (𝐹𝑥)) ↔ (𝑥𝐴𝑥𝐹𝑦)))
116, 10bitr4d 271 . . . . 5 (𝐹 Fn 𝐴 → (𝑥𝐹𝑦 ↔ (𝑥𝐴𝑦 = (𝐹𝑥))))
1211opabbidv 4868 . . . 4 (𝐹 Fn 𝐴 → {⟨𝑥, 𝑦⟩ ∣ 𝑥𝐹𝑦} = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 = (𝐹𝑥))})
133, 12eqtrd 2794 . . 3 (𝐹 Fn 𝐴𝐹 = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 = (𝐹𝑥))})
14 df-mpt 4882 . . 3 (𝑥𝐴 ↦ (𝐹𝑥)) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 = (𝐹𝑥))}
1513, 14syl6eqr 2812 . 2 (𝐹 Fn 𝐴𝐹 = (𝑥𝐴 ↦ (𝐹𝑥)))
16 fvex 6363 . . . 4 (𝐹𝑥) ∈ V
17 eqid 2760 . . . 4 (𝑥𝐴 ↦ (𝐹𝑥)) = (𝑥𝐴 ↦ (𝐹𝑥))
1816, 17fnmpti 6183 . . 3 (𝑥𝐴 ↦ (𝐹𝑥)) Fn 𝐴
19 fneq1 6140 . . 3 (𝐹 = (𝑥𝐴 ↦ (𝐹𝑥)) → (𝐹 Fn 𝐴 ↔ (𝑥𝐴 ↦ (𝐹𝑥)) Fn 𝐴))
2018, 19mpbiri 248 . 2 (𝐹 = (𝑥𝐴 ↦ (𝐹𝑥)) → 𝐹 Fn 𝐴)
2115, 20impbii 199 1 (𝐹 Fn 𝐴𝐹 = (𝑥𝐴 ↦ (𝐹𝑥)))
Colors of variables: wff setvar class
Syntax hints:  wb 196  wa 383   = wceq 1632  wcel 2139   class class class wbr 4804  {copab 4864  cmpt 4881  Rel wrel 5271   Fn wfn 6044  cfv 6049
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-sep 4933  ax-nul 4941  ax-pr 5055
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ral 3055  df-rex 3056  df-rab 3059  df-v 3342  df-sbc 3577  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-nul 4059  df-if 4231  df-sn 4322  df-pr 4324  df-op 4328  df-uni 4589  df-br 4805  df-opab 4865  df-mpt 4882  df-id 5174  df-xp 5272  df-rel 5273  df-cnv 5274  df-co 5275  df-dm 5276  df-iota 6012  df-fun 6051  df-fn 6052  df-fv 6057
This theorem is referenced by:  fnrnfv  6405  feqmptd  6412  dffn5f  6415  eqfnfv  6475  fndmin  6488  fcompt  6564  funiun  6576  resfunexg  6644  eufnfv  6655  nvocnv  6701  fnov  6934  offveqb  7085  caofinvl  7090  oprabco  7430  df1st2  7432  df2nd2  7433  curry1  7438  curry2  7441  resixpfo  8114  pw2f1olem  8231  marypha2lem3  8510  seqof  13072  prmrec  15848  prdsbascl  16365  xpsaddlem  16457  xpsvsca  16461  oppccatid  16600  fuclid  16847  fucrid  16848  curfuncf  17099  yonedainv  17142  yonffthlem  17143  prdsidlem  17543  pws0g  17547  prdsinvlem  17745  gsummptmhm  18560  staffn  19071  prdslmodd  19191  ofco2  20479  1mavmul  20576  cnmpt1st  21693  cnmpt2nd  21694  ptunhmeo  21833  xpsxmetlem  22405  xpsmet  22408  itg2split  23735  pserulm  24395  pserdvlem2  24401  logcn  24613  logblog  24750  emcllem5  24946  gamcvg2lem  25005  crctcshlem4  26944  eucrct2eupth  27418  fcomptf  29788  gsummpt2d  30111  pl1cn  30331  esumpcvgval  30470  esumcvgsum  30480  eulerpartgbij  30764  dstfrvclim1  30869  ptpconn  31543  knoppcnlem8  32817  knoppcnlem11  32820  curfv  33720  ovoliunnfl  33782  voliunnfl  33784  fnopabco  33848  upixp  33855  prdsbnd  33923  prdstotbnd  33924  prdsbnd2  33925  fgraphopab  38308  expgrowthi  39052  expgrowth  39054  uzmptshftfval  39065  dvcosre  40647  fourierdlem56  40900  fourierdlem62  40906  fdmdifeqresdif  42648  offvalfv  42649
  Copyright terms: Public domain W3C validator