Theorem dffn5 6937

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 6635	. . . . 5 ⊢ (𝐹 Fn 𝐴 → Rel 𝐹)
2		dfrel4v 6187	. . . . 5 ⊢ (Rel 𝐹 ↔ 𝐹 = {⟨𝑥, 𝑦⟩ ∣ 𝑥𝐹𝑦})
3	1, 2	sylib 221	. . . 4 ⊢ (𝐹 Fn 𝐴 → 𝐹 = {⟨𝑥, 𝑦⟩ ∣ 𝑥𝐹𝑦})
4		fnbr 6641	. . . . . . . 8 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑥𝐹𝑦) → 𝑥 ∈ 𝐴)
5	4	ex 417	. . . . . . 7 ⊢ (𝐹 Fn 𝐴 → (𝑥𝐹𝑦 → 𝑥 ∈ 𝐴))
6	5	pm4.71rd 571	. . . . . 6 ⊢ (𝐹 Fn 𝐴 → (𝑥𝐹𝑦 ↔ (𝑥 ∈ 𝐴 ∧ 𝑥𝐹𝑦)))
7		eqcom 2776	. . . . . . . 8 ⊢ (𝑦 = (𝐹‘𝑥) ↔ (𝐹‘𝑥) = 𝑦)
8		fnbrfvb 6929	. . . . . . . 8 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑥 ∈ 𝐴) → ((𝐹‘𝑥) = 𝑦 ↔ 𝑥𝐹𝑦))
9	7, 8	bitrid 286	. . . . . . 7 ⊢ ((𝐹 Fn 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝑦 = (𝐹‘𝑥) ↔ 𝑥𝐹𝑦))
10	9	pm5.32da 589	. . . . . 6 ⊢ (𝐹 Fn 𝐴 → ((𝑥 ∈ 𝐴 ∧ 𝑦 = (𝐹‘𝑥)) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥𝐹𝑦)))
11	6, 10	bitr4d 285	. . . . 5 ⊢ (𝐹 Fn 𝐴 → (𝑥𝐹𝑦 ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 = (𝐹‘𝑥))))
12	11	opabbidv 5178	. . . 4 ⊢ (𝐹 Fn 𝐴 → {⟨𝑥, 𝑦⟩ ∣ 𝑥𝐹𝑦} = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = (𝐹‘𝑥))})
13	3, 12	eqtrd 2804	. . 3 ⊢ (𝐹 Fn 𝐴 → 𝐹 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = (𝐹‘𝑥))})
14		df-mpt 5194	. . 3 ⊢ (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = (𝐹‘𝑥))}
15	13, 14	eqtr4di 2822	. 2 ⊢ (𝐹 Fn 𝐴 → 𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)))
16		fvex 6892	. . . 4 ⊢ (𝐹‘𝑥) ∈ V
17		eqid 2769	. . . 4 ⊢ (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥))
18	16, 17	fnmpti 6676	. . 3 ⊢ (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) Fn 𝐴
19		fneq1 6624	. . 3 ⊢ (𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) → (𝐹 Fn 𝐴 ↔ (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) Fn 𝐴))
20	18, 19	mpbiri 261	. 2 ⊢ (𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) → 𝐹 Fn 𝐴)
21	15, 20	impbii 212	1 ⊢ (𝐹 Fn 𝐴 ↔ 𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)))

Syntax hints:   ↔ wb 209   ∧ wa 400   = wceq 1567   ∈ wcel 2149   class class class wbr 5110  {copab 5174   ↦ cmpt 5193  Rel wrel 5664   Fn wfn 6528  ‘cfv 6533

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-sep 5258  ax-nul 5268  ax-pr 5402

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ne 2965  df-ral 3086  df-rex 3096  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4874  df-br 5111  df-opab 5175  df-mpt 5194  df-id 5554  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-iota 6489  df-fun 6535  df-fn 6536  df-fv 6541

This theorem is referenced by:  fnrnfv  6938  feqmptd  6947  dffn5f  6950  eqfnfv  7023  fndmin  7038  fcompt  7127  funiun  7141  resfunexg  7211  eufnfv  7225  nvocnv  7277  fnov  7539  offvalfv  7694  offveqb  7699  caofinvl  7704  oprabco  8087  df1st2  8089  df2nd2  8090  curry1  8095  curry2  8098  resixpfo  8930  pw2f1olem  9065  marypha2lem3  9393  seqof  14091  prmrec  16978  prdsbascl  17532  xpsaddlem  17623  xpsvsca  17627  oppccatid  17771  fuclid  18022  fucrid  18023  curfuncf  18290  yonedainv  18333  yonffthlem  18334  prdsidlem  18823  pws0g  18827  prdsinvlem  19111  gsummptmhm  20006  staffn  20920  prdslmodd  21064  ofco2  22573  1mavmul  22670  cnmpt1st  23790  cnmpt2nd  23791  ptunhmeo  23930  xpsxmetlem  24501  xpsmet  24504  itg2split  25873  pserulm  26547  pserdvlem2  26553  logcn  26774  logblog  26919  emcllem5  27126  gamcvg2lem  27185  crctcshlem4  30106  eucrct2eupth  30533  fcomptf  32940  gsummpt2d  33306  esplyfval3  33903  pl1cn  34286  esumpcvgval  34409  esumcvgsum  34419  eulerpartgbij  34703  dstfrvclim1  34809  ptpconn  35620  knoppcnlem8  36974  knoppcnlem11  36977  ctbssinf  37935  curfv  38134  ovoliunnfl  38196  voliunnfl  38198  fnopabco  38257  upixp  38263  prdsbnd  38327  prdstotbnd  38328  prdsbnd2  38329  sticksstones12a  42809  sticksstones12  42810  sticksstones19  42817  fgraphopab  43815  rp-tfslim  43965  expgrowthi  44928  expgrowth  44930  uzmptshftfval  44941  dvcosre  46511  fourierdlem56  46761  fourierdlem62  46767  fundcmpsurbijinjpreimafv  48038  fundcmpsurinjimaid  48042  fdmdifeqresdif  49000  isnatd  49879