Theorem dffn5 6892

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 6594	. . . . 5 ⊢ (𝐹 Fn 𝐴 → Rel 𝐹)
2		dfrel4v 6148	. . . . 5 ⊢ (Rel 𝐹 ↔ 𝐹 = {⟨𝑥, 𝑦⟩ ∣ 𝑥𝐹𝑦})
3	1, 2	sylib 218	. . . 4 ⊢ (𝐹 Fn 𝐴 → 𝐹 = {⟨𝑥, 𝑦⟩ ∣ 𝑥𝐹𝑦})
4		fnbr 6600	. . . . . . . 8 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑥𝐹𝑦) → 𝑥 ∈ 𝐴)
5	4	ex 412	. . . . . . 7 ⊢ (𝐹 Fn 𝐴 → (𝑥𝐹𝑦 → 𝑥 ∈ 𝐴))
6	5	pm4.71rd 562	. . . . . 6 ⊢ (𝐹 Fn 𝐴 → (𝑥𝐹𝑦 ↔ (𝑥 ∈ 𝐴 ∧ 𝑥𝐹𝑦)))
7		eqcom 2743	. . . . . . . 8 ⊢ (𝑦 = (𝐹‘𝑥) ↔ (𝐹‘𝑥) = 𝑦)
8		fnbrfvb 6884	. . . . . . . 8 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑥 ∈ 𝐴) → ((𝐹‘𝑥) = 𝑦 ↔ 𝑥𝐹𝑦))
9	7, 8	bitrid 283	. . . . . . 7 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝑦 = (𝐹‘𝑥) ↔ 𝑥𝐹𝑦))
10	9	pm5.32da 579	. . . . . 6 ⊢ (𝐹 Fn 𝐴 → ((𝑥 ∈ 𝐴 ∧ 𝑦 = (𝐹‘𝑥)) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥𝐹𝑦)))
11	6, 10	bitr4d 282	. . . . 5 ⊢ (𝐹 Fn 𝐴 → (𝑥𝐹𝑦 ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 = (𝐹‘𝑥))))
12	11	opabbidv 5164	. . . 4 ⊢ (𝐹 Fn 𝐴 → {⟨𝑥, 𝑦⟩ ∣ 𝑥𝐹𝑦} = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = (𝐹‘𝑥))})
13	3, 12	eqtrd 2771	. . 3 ⊢ (𝐹 Fn 𝐴 → 𝐹 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = (𝐹‘𝑥))})
14		df-mpt 5180	. . 3 ⊢ (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = (𝐹‘𝑥))}
15	13, 14	eqtr4di 2789	. 2 ⊢ (𝐹 Fn 𝐴 → 𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)))
16		fvex 6847	. . . 4 ⊢ (𝐹‘𝑥) ∈ V
17		eqid 2736	. . . 4 ⊢ (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥))
18	16, 17	fnmpti 6635	. . 3 ⊢ (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) Fn 𝐴
19		fneq1 6583	. . 3 ⊢ (𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) → (𝐹 Fn 𝐴 ↔ (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) Fn 𝐴))
20	18, 19	mpbiri 258	. 2 ⊢ (𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) → 𝐹 Fn 𝐴)
21	15, 20	impbii 209	1 ⊢ (𝐹 Fn 𝐴 ↔ 𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)))

Syntax hints:   ↔ wb 206   ∧ wa 395   = wceq 1541   ∈ wcel 2113   class class class wbr 5098  {copab 5160   ↦ cmpt 5179  Rel wrel 5629   Fn wfn 6487  ‘cfv 6492

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 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2184  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pr 5377

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-opab 5161  df-mpt 5180  df-id 5519  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-iota 6448  df-fun 6494  df-fn 6495  df-fv 6500

This theorem is referenced by:  fnrnfv  6893  feqmptd  6902  dffn5f  6905  eqfnfv  6976  fndmin  6990  fcompt  7078  funiun  7092  resfunexg  7161  eufnfv  7175  nvocnv  7227  fnov  7489  offvalfv  7644  offveqb  7649  caofinvl  7654  oprabco  8038  df1st2  8040  df2nd2  8041  curry1  8046  curry2  8049  resixpfo  8874  pw2f1olem  9009  marypha2lem3  9340  seqof  13982  prmrec  16850  prdsbascl  17403  xpsaddlem  17494  xpsvsca  17498  oppccatid  17642  fuclid  17893  fucrid  17894  curfuncf  18161  yonedainv  18204  yonffthlem  18205  prdsidlem  18694  pws0g  18698  prdsinvlem  18979  gsummptmhm  19869  staffn  20776  prdslmodd  20920  ofco2  22395  1mavmul  22492  cnmpt1st  23612  cnmpt2nd  23613  ptunhmeo  23752  xpsxmetlem  24323  xpsmet  24326  itg2split  25706  pserulm  26387  pserdvlem2  26394  logcn  26612  logblog  26758  emcllem5  26966  gamcvg2lem  27025  crctcshlem4  29893  eucrct2eupth  30320  fcomptf  32736  gsummpt2d  33132  esplyfval3  33730  pl1cn  34112  esumpcvgval  34235  esumcvgsum  34245  eulerpartgbij  34529  dstfrvclim1  34635  ptpconn  35427  knoppcnlem8  36700  knoppcnlem11  36703  ctbssinf  37611  curfv  37801  ovoliunnfl  37863  voliunnfl  37865  fnopabco  37924  upixp  37930  prdsbnd  37994  prdstotbnd  37995  prdsbnd2  37996  sticksstones12a  42411  sticksstones12  42412  sticksstones19  42419  fgraphopab  43445  rp-tfslim  43595  expgrowthi  44574  expgrowth  44576  uzmptshftfval  44587  dvcosre  46156  fourierdlem56  46406  fourierdlem62  46412  fundcmpsurbijinjpreimafv  47653  fundcmpsurinjimaid  47657  fdmdifeqresdif  48588  isnatd  49468