Theorem dffn5 6241

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 5989	. . . . 5 ⊢ (𝐹 Fn 𝐴 → Rel 𝐹)
2		dfrel4v 5584	. . . . 5 ⊢ (Rel 𝐹 ↔ 𝐹 = {⟨𝑥, 𝑦⟩ ∣ 𝑥𝐹𝑦})
3	1, 2	sylib 208	. . . 4 ⊢ (𝐹 Fn 𝐴 → 𝐹 = {⟨𝑥, 𝑦⟩ ∣ 𝑥𝐹𝑦})
4		fnbr 5993	. . . . . . . 8 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑥𝐹𝑦) → 𝑥 ∈ 𝐴)
5	4	ex 450	. . . . . . 7 ⊢ (𝐹 Fn 𝐴 → (𝑥𝐹𝑦 → 𝑥 ∈ 𝐴))
6	5	pm4.71rd 667	. . . . . 6 ⊢ (𝐹 Fn 𝐴 → (𝑥𝐹𝑦 ↔ (𝑥 ∈ 𝐴 ∧ 𝑥𝐹𝑦)))
7		eqcom 2629	. . . . . . . 8 ⊢ (𝑦 = (𝐹‘𝑥) ↔ (𝐹‘𝑥) = 𝑦)
8		fnbrfvb 6236	. . . . . . . 8 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑥 ∈ 𝐴) → ((𝐹‘𝑥) = 𝑦 ↔ 𝑥𝐹𝑦))
9	7, 8	syl5bb 272	. . . . . . 7 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝑦 = (𝐹‘𝑥) ↔ 𝑥𝐹𝑦))
10	9	pm5.32da 673	. . . . . 6 ⊢ (𝐹 Fn 𝐴 → ((𝑥 ∈ 𝐴 ∧ 𝑦 = (𝐹‘𝑥)) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥𝐹𝑦)))
11	6, 10	bitr4d 271	. . . . 5 ⊢ (𝐹 Fn 𝐴 → (𝑥𝐹𝑦 ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 = (𝐹‘𝑥))))
12	11	opabbidv 4716	. . . 4 ⊢ (𝐹 Fn 𝐴 → {⟨𝑥, 𝑦⟩ ∣ 𝑥𝐹𝑦} = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = (𝐹‘𝑥))})
13	3, 12	eqtrd 2656	. . 3 ⊢ (𝐹 Fn 𝐴 → 𝐹 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = (𝐹‘𝑥))})
14		df-mpt 4730	. . 3 ⊢ (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = (𝐹‘𝑥))}
15	13, 14	syl6eqr 2674	. 2 ⊢ (𝐹 Fn 𝐴 → 𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)))
16		fvex 6201	. . . 4 ⊢ (𝐹‘𝑥) ∈ V
17		eqid 2622	. . . 4 ⊢ (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥))
18	16, 17	fnmpti 6022	. . 3 ⊢ (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) Fn 𝐴
19		fneq1 5979	. . 3 ⊢ (𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) → (𝐹 Fn 𝐴 ↔ (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) Fn 𝐴))
20	18, 19	mpbiri 248	. 2 ⊢ (𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) → 𝐹 Fn 𝐴)
21	15, 20	impbii 199	1 ⊢ (𝐹 Fn 𝐴 ↔ 𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)))

Syntax hints:   ↔ wb 196   ∧ wa 384   = wceq 1483   ∈ wcel 1990   class class class wbr 4653  {copab 4712   ↦ cmpt 4729  Rel wrel 5119   Fn wfn 5883  ‘cfv 5888

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pr 4906

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-sbc 3436  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-opab 4713  df-mpt 4730  df-id 5024  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-iota 5851  df-fun 5890  df-fn 5891  df-fv 5896

This theorem is referenced by:  fnrnfv  6242  feqmptd  6249  dffn5f  6252  eqfnfv  6311  fndmin  6324  fcompt  6400  funiun  6412  resfunexg  6479  eufnfv  6491  nvocnv  6537  fnov  6768  offveqb  6919  caofinvl  6924  oprabco  7261  df1st2  7263  df2nd2  7264  curry1  7269  curry2  7272  resixpfo  7946  pw2f1olem  8064  marypha2lem3  8343  seqof  12858  prmrec  15626  prdsbascl  16143  xpsaddlem  16235  xpsvsca  16239  oppccatid  16379  fuclid  16626  fucrid  16627  curfuncf  16878  yonedainv  16921  yonffthlem  16922  prdsidlem  17322  pws0g  17326  prdsinvlem  17524  gsummptmhm  18340  staffn  18849  prdslmodd  18969  ofco2  20257  1mavmul  20354  cnmpt1st  21471  cnmpt2nd  21472  ptunhmeo  21611  xpsxmetlem  22184  xpsmet  22187  itg2split  23516  pserulm  24176  pserdvlem2  24182  logcn  24393  logblog  24530  emcllem5  24726  gamcvg2lem  24785  crctcshlem4  26712  eucrct2eupth  27105  fcomptf  29458  gsummpt2d  29781  pl1cn  30001  esumpcvgval  30140  esumcvgsum  30150  eulerpartgbij  30434  dstfrvclim1  30539  ptpconn  31215  knoppcnlem8  32490  knoppcnlem11  32493  curfv  33389  ovoliunnfl  33451  voliunnfl  33453  fnopabco  33517  upixp  33524  prdsbnd  33592  prdstotbnd  33593  prdsbnd2  33594  fgraphopab  37788  expgrowthi  38532  expgrowth  38534  uzmptshftfval  38545  dvcosre  40126  fourierdlem56  40379  fourierdlem62  40385  fdmdifeqresdif  42120  offvalfv  42121