Theorem dffn5 6974

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 6671	. . . . 5 ⊢ (𝐹 Fn 𝐴 → Rel 𝐹)
2		dfrel4v 6200	. . . . 5 ⊢ (Rel 𝐹 ↔ 𝐹 = {⟨𝑥, 𝑦⟩ ∣ 𝑥𝐹𝑦})
3	1, 2	sylib 221	. . . 4 ⊢ (𝐹 Fn 𝐴 → 𝐹 = {⟨𝑥, 𝑦⟩ ∣ 𝑥𝐹𝑦})
4		fnbr 6677	. . . . . . . 8 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑥𝐹𝑦) → 𝑥 ∈ 𝐴)
5	4	ex 418	. . . . . . 7 ⊢ (𝐹 Fn 𝐴 → (𝑥𝐹𝑦 → 𝑥 ∈ 𝐴))
6	5	pm4.71rd 572	. . . . . 6 ⊢ (𝐹 Fn 𝐴 → (𝑥𝐹𝑦 ↔ (𝑥 ∈ 𝐴 ∧ 𝑥𝐹𝑦)))
7		eqcom 2770	. . . . . . . 8 ⊢ (𝑦 = (𝐹‘𝑥) ↔ (𝐹‘𝑥) = 𝑦)
8		fnbrfvb 6966	. . . . . . . 8 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑥 ∈ 𝐴) → ((𝐹‘𝑥) = 𝑦 ↔ 𝑥𝐹𝑦))
9	7, 8	bitrid 286	. . . . . . 7 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝑦 = (𝐹‘𝑥) ↔ 𝑥𝐹𝑦))
10	9	pm5.32da 590	. . . . . 6 ⊢ (𝐹 Fn 𝐴 → ((𝑥 ∈ 𝐴 ∧ 𝑦 = (𝐹‘𝑥)) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥𝐹𝑦)))
11	6, 10	bitr4d 285	. . . . 5 ⊢ (𝐹 Fn 𝐴 → (𝑥𝐹𝑦 ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 = (𝐹‘𝑥))))
12	11	opabbidv 5177	. . . 4 ⊢ (𝐹 Fn 𝐴 → {⟨𝑥, 𝑦⟩ ∣ 𝑥𝐹𝑦} = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = (𝐹‘𝑥))})
13	3, 12	eqtrd 2798	. . 3 ⊢ (𝐹 Fn 𝐴 → 𝐹 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = (𝐹‘𝑥))})
14		df-mpt 5193	. . 3 ⊢ (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = (𝐹‘𝑥))}
15	13, 14	eqtr4di 2816	. 2 ⊢ (𝐹 Fn 𝐴 → 𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)))
16		fvex 6929	. . . 4 ⊢ (𝐹‘𝑥) ∈ V
17		eqid 2763	. . . 4 ⊢ (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥))
18	16, 17	fnmpti 6712	. . 3 ⊢ (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) Fn 𝐴
19		fneq1 6660	. . 3 ⊢ (𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) → (𝐹 Fn 𝐴 ↔ (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) Fn 𝐴))
20	18, 19	mpbiri 261	. 2 ⊢ (𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) → 𝐹 Fn 𝐴)
21	15, 20	impbii 212	1 ⊢ (𝐹 Fn 𝐴 ↔ 𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)))

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401   = wceq 1570   ∈ wcel 2147   class class class wbr 5108  {copab 5173   ↦ cmpt 5192  Rel wrel 5663   Fn wfn 6561  ‘cfv 6566

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5255  ax-nul 5266  ax-pr 5398

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4841  df-uni 4873  df-br 5109  df-opab 5174  df-mpt 5193  df-id 5553  df-xp 5664  df-rel 5665  df-cnv 5666  df-co 5667  df-dm 5668  df-iota 6520  df-fun 6568  df-fn 6569  df-fv 6574

This theorem is used by:  fnrnfv  6975  feqmptd  6984  dffn5f  6987  eqfnfv  7060  fndmin  7075  fcompt  7166  funiun  7182  resfunexg  7252  eufnfv  7266  nvocnv  7320  fnov  7582  offvalfv  7747  offveqb  7752  caofinvl  7757  oprabco  8143  df1st2  8146  df2nd2  8147  curry1  8152  curry2  8155  curfv  8930  resixpfo  9002  pw2f1olem  9138  marypha2lem3  9466  seqof  14242  prmrec  17144  prdsbascl  17704  xpsaddlem  17795  xpsvsca  17799  oppccatid  17943  fuclid  18194  fucrid  18195  curfuncf  18462  yonedainv  18505  yonffthlem  18506  prdsidlem  19013  pws0g  19017  prdsinvlem  19309  gsummptmhm  20205  staffn  21151  prdslmodd  21295  ofco2  22821  1mavmul  22918  cnmpt1st  24042  cnmpt2nd  24043  ptunhmeo  24182  xpsxmetlem  24753  xpsmet  24756  itg2split  26125  pserulm  26806  pserdvlem2  26812  logcn  27032  logblog  27177  emcllem5  27384  gamcvg2lem  27443  crctcshlem4  30466  eucrct2eupth  30903  fcomptf  33350  gsummpt2d  33709  esplyfval3  34315  pl1cn  34698  esumpcvgval  34821  esumcvgsum  34831  eulerpartgbij  35115  dstfrvclim1  35221  ptpconn  36206  knoppcnlem8  37581  knoppcnlem11  37584  ctbssinf  38597  ovoliunnfl  38848  voliunnfl  38850  fnopabco  38925  upixp  38931  prdsbnd  38993  prdstotbnd  38994  prdsbnd2  38995  sticksstones12a  43473  sticksstones12  43474  sticksstones19  43481  fgraphopab  44466  rp-tfslim  44616  expgrowthi  45578  expgrowth  45580  uzmptshftfval  45591  dvcosre  47195  fourierdlem56  47445  fourierdlem62  47451  fundcmpsurbijinjpreimafv  48762  fundcmpsurinjimaid  48766  fdmdifeqresdif  49785  elixpmpt  50335  isnatd  50670  veronesematrowd  51409