Theorem dffn5 6888

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.

Step	Hyp	Ref	Expression
1		fnrel 6590	. . . . 5 ⊢ (𝐹 Fn 𝐴 → Rel 𝐹)
2		dfrel4v 6144	. . . . 5 ⊢ (Rel 𝐹 ↔ 𝐹 = {⟨𝑥, 𝑦⟩ ∣ 𝑥𝐹𝑦})
3	1, 2	sylib 220	. . . 4 ⊢ (𝐹 Fn 𝐴 → 𝐹 = {⟨𝑥, 𝑦⟩ ∣ 𝑥𝐹𝑦})
4		fnbr 6596	. . . . . . . 8 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑥𝐹𝑦) → 𝑥 ∈ 𝐴)
5	4	ex 414	. . . . . . 7 ⊢ (𝐹 Fn 𝐴 → (𝑥𝐹𝑦 → 𝑥 ∈ 𝐴))
6	5	pm4.71rd 568	. . . . . 6 ⊢ (𝐹 Fn 𝐴 → (𝑥𝐹𝑦 ↔ (𝑥 ∈ 𝐴 ∧ 𝑥𝐹𝑦)))
7		eqcom 2748	. . . . . . . 8 ⊢ (𝑦 = (𝐹‘𝑥) ↔ (𝐹‘𝑥) = 𝑦)
8		fnbrfvb 6880	. . . . . . . 8 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑥 ∈ 𝐴) → ((𝐹‘𝑥) = 𝑦 ↔ 𝑥𝐹𝑦))
9	7, 8	bitrid 285	. . . . . . 7 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝑦 = (𝐹‘𝑥) ↔ 𝑥𝐹𝑦))
10	9	pm5.32da 585	. . . . . 6 ⊢ (𝐹 Fn 𝐴 → ((𝑥 ∈ 𝐴 ∧ 𝑦 = (𝐹‘𝑥)) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥𝐹𝑦)))
11	6, 10	bitr4d 284	. . . . 5 ⊢ (𝐹 Fn 𝐴 → (𝑥𝐹𝑦 ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 = (𝐹‘𝑥))))
12	11	opabbidv 5140	. . . 4 ⊢ (𝐹 Fn 𝐴 → {⟨𝑥, 𝑦⟩ ∣ 𝑥𝐹𝑦} = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = (𝐹‘𝑥))})
13	3, 12	eqtrd 2776	. . 3 ⊢ (𝐹 Fn 𝐴 → 𝐹 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = (𝐹‘𝑥))})
14		df-mpt 5156	. . 3 ⊢ (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = (𝐹‘𝑥))}
15	13, 14	eqtr4di 2794	. 2 ⊢ (𝐹 Fn 𝐴 → 𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)))
16		fvex 6843	. . . 4 ⊢ (𝐹‘𝑥) ∈ V
17		eqid 2741	. . . 4 ⊢ (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥))
18	16, 17	fnmpti 6631	. . 3 ⊢ (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) Fn 𝐴
19		fneq1 6579	. . 3 ⊢ (𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) → (𝐹 Fn 𝐴 ↔ (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) Fn 𝐴))
20	18, 19	mpbiri 260	. 2 ⊢ (𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) → 𝐹 Fn 𝐴)
21	15, 20	impbii 211	1 ⊢ (𝐹 Fn 𝐴 ↔ 𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)))

Syntax hints:   ↔ wb 208   ∧ wa 397   = wceq 1548   ∈ wcel 2121   class class class wbr 5074  {copab 5136   ↦ cmpt 5155  Rel wrel 5625   Fn wfn 6483  ‘cfv 6488

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1975  ax-7 2016  ax-8 2123  ax-9 2131  ax-10 2154  ax-11 2170  ax-12 2191  ax-ext 2713  ax-sep 5220  ax-nul 5230  ax-pr 5364

This theorem depends on definitions:  df-bi 209  df-an 398  df-or 855  df-3an 1095  df-tru 1551  df-fal 1561  df-ex 1788  df-nf 1792  df-sb 2075  df-mo 2545  df-eu 2575  df-clab 2720  df-cleq 2733  df-clel 2816  df-nfc 2890  df-ne 2937  df-ral 3056  df-rex 3066  df-rab 3394  df-v 3435  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-nul 4264  df-if 4457  df-sn 4558  df-pr 4560  df-op 4564  df-uni 4841  df-br 5075  df-opab 5137  df-mpt 5156  df-id 5515  df-xp 5626  df-rel 5627  df-cnv 5628  df-co 5629  df-dm 5630  df-iota 6444  df-fun 6490  df-fn 6491  df-fv 6496

This theorem is referenced by:  fnrnfv  6889  feqmptd  6898  dffn5f  6901  eqfnfv  6974  fndmin  6989  fcompt  7078  funiun  7092  resfunexg  7162  eufnfv  7176  nvocnv  7228  fnov  7490  offvalfv  7645  offveqb  7650  caofinvl  7655  oprabco  8037  df1st2  8039  df2nd2  8040  curry1  8045  curry2  8048  resixpfo  8878  pw2f1olem  9013  marypha2lem3  9344  seqof  14016  prmrec  16888  prdsbascl  17441  xpsaddlem  17532  xpsvsca  17536  oppccatid  17680  fuclid  17931  fucrid  17932  curfuncf  18199  yonedainv  18242  yonffthlem  18243  prdsidlem  18732  pws0g  18736  prdsinvlem  19020  gsummptmhm  19909  staffn  20818  prdslmodd  20962  ofco2  22437  1mavmul  22534  cnmpt1st  23654  cnmpt2nd  23655  ptunhmeo  23794  xpsxmetlem  24365  xpsmet  24368  itg2split  25737  pserulm  26408  pserdvlem2  26414  logcn  26632  logblog  26777  emcllem5  26984  gamcvg2lem  27043  crctcshlem4  29908  eucrct2eupth  30335  fcomptf  32752  gsummpt2d  33132  esplyfval3  33766  pl1cn  34149  esumpcvgval  34272  esumcvgsum  34282  eulerpartgbij  34566  dstfrvclim1  34672  ptpconn  35474  knoppcnlem8  36819  knoppcnlem11  36822  ctbssinf  37781  curfv  37980  ovoliunnfl  38042  voliunnfl  38044  fnopabco  38103  upixp  38109  prdsbnd  38173  prdstotbnd  38174  prdsbnd2  38175  sticksstones12a  42655  sticksstones12  42656  sticksstones19  42663  fgraphopab  43661  rp-tfslim  43811  expgrowthi  44790  expgrowth  44792  uzmptshftfval  44803  dvcosre  46367  fourierdlem56  46617  fourierdlem62  46623  fundcmpsurbijinjpreimafv  47894  fundcmpsurinjimaid  47898  fdmdifeqresdif  48845  isnatd  49725