Theorem dffn5 5918

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

Distinct variable groups:   ,   ,

Proof of Theorem dffn5

Dummy variable is distinct from all other variables.

Step	Hyp	Ref	Expression
1		fnrel 5684	. . . . 5
2		dfrel4v 5463	. . . . 5
3	1, 2	sylib 196	. . . 4
4		fnbr 5688	. . . . . . . 8
5	4	ex 434	. . . . . . 7
6	5	pm4.71rd 635	. . . . . 6
7		eqcom 2466	. . . . . . . 8
8		fnbrfvb 5913	. . . . . . . 8
9	7, 8	syl5bb 257	. . . . . . 7
10	9	pm5.32da 641	. . . . . 6
11	6, 10	bitr4d 256	. . . . 5
12	11	opabbidv 4515	. . . 4
13	3, 12	eqtrd 2498	. . 3
14		df-mpt 4512	. . 3
15	13, 14	syl6eqr 2516	. 2
16		fvex 5881	. . . 4
17		eqid 2457	. . . 4
18	16, 17	fnmpti 5714	. . 3
19		fneq1 5674	. . 3
20	18, 19	mpbiri 233	. 2
21	15, 20	impbii 188	1

Syntax hints:  <->wb 184  /\wa 369  =wceq 1395  e.wcel 1818   class class class wbr 4452  {copab 4509  e.cmpt 4510  Relwrel 5009  Fnwfn 5588  `cfv 5593

This theorem is referenced by:  fnrnfv  5919  feqmptd  5926  dffn5f  5928  eqfnfv  5981  fndmin  5994  fcompt  6067  resfunexg  6137  eufnfv  6146  nvocnv  6187  fnov  6410  offveqb  6562  caofinvl  6567  oprabco  6884  df1st2  6886  df2nd2  6887  curry1  6892  curry2  6895  resixpfo  7527  pw2f1olem  7641  marypha2lem3  7917  seqof  12164  prmrec  14440  prdsbascl  14880  xpsaddlem  14972  xpsvsca  14976  oppccatid  15114  fuclid  15335  fucrid  15336  curfuncf  15507  yonedainv  15550  yonffthlem  15551  prdsidlem  15952  pws0g  15956  prdsinvlem  16178  gsummptmhm  16963  staffn  17498  prdslmodd  17615  ofco2  18953  1mavmul  19050  cnmpt1st  20169  cnmpt2nd  20170  ptunhmeo  20309  xpsxmetlem  20882  xpsmet  20885  itg2split  22156  pserulm  22817  pserdvlem2  22823  logcn  23028  emcllem5  23329  fcomptf  27503  pl1cn  27937  esumpcvgval  28084  eulerpartgbij  28311  dstfrvclim1  28416  gamcvg2lem  28601  ptpcon  28678  ovoliunnfl  30056  voliunnfl  30058  dvtanlem  30064  fnopabco  30213  upixp  30220  prdsbnd  30289  prdstotbnd  30290  prdsbnd2  30291  fgraphopab  31170  expgrowthi  31238  expgrowth  31240  uzmptshftfval  31251  dvcosre  31706  fourierdlem56  31945  fourierdlem62  31951  fdmdifeqresdif  32931  offvalfv  32932

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-9 1822  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-sep 4573  ax-nul 4581  ax-pr 4691

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-eu 2286  df-mo 2287  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3111  df-sbc 3328  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-sn 4030  df-pr 4032  df-op 4036  df-uni 4250  df-br 4453  df-opab 4511  df-mpt 4512  df-id 4800  df-xp 5010  df-rel 5011  df-cnv 5012  df-co 5013  df-dm 5014  df-iota 5556  df-fun 5595  df-fn 5596  df-fv 5601