Theorem feqmptd 6249

Description: Deduction form of dffn5 6241. (Contributed by Mario Carneiro, 8-Jan-2015.)

Hypothesis

Ref	Expression
feqmptd.1	|- ( ph -> F : A --> B )

Assertion

Ref	Expression
feqmptd	|- ( ph -> F = ( x e. A |-> ( F ` x ) ) )

Distinct variable groups:   x, A   x, F

Allowed substitution hints:   ph( x)   B( x)

Proof of Theorem feqmptd

Step	Hyp	Ref	Expression
1		feqmptd.1	. . 3 |- ( ph -> F : A --> B )
2		ffn 6045	. . 3 |- ( F : A --> B -> F Fn A )
3	1, 2	syl 17	. 2 |- ( ph -> F Fn A )
4		dffn5 6241	. 2 |- ( F Fn A <-> F = ( x e. A |-> ( F ` x ) ) )
5	3, 4	sylib 208	1 |- ( ph -> F = ( x e. A |-> ( F ` x ) ) )

Syntax hints:   -> wi 4   = wceq 1483   |-> cmpt 4729   Fn wfn 5883   -->wf 5884   ` 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-f 5892  df-fv 5896

This theorem is referenced by:  feqresmpt  6250  cofmpt  6399  fcoconst  6401  ofco  6917  caofinvl  6924  caofcom  6929  caofass  6931  caofdi  6933  caofdir  6934  caonncan  6935  suppssof1  7328  mapxpen  8126  xpmapenlem  8127  cantnfp1  8578  cantnflem1  8586  cnfcom2lem  8598  infxpenc  8841  pwfseqlem5  9485  gruf  9633  ccatco  13581  cnrecnv  13905  lo1o12  14264  rlimclim1  14276  rlimuni  14281  lo1resb  14295  rlimresb  14296  o1resb  14297  rlimcn1  14319  rlimcn1b  14320  rlimo1  14347  o1rlimmul  14349  caucvgr  14406  ackbijnn  14560  bitsf1ocnv  15166  ramcl  15733  pwsplusgval  16150  pwsmulrval  16151  pwsvscafval  16154  setcepi  16738  prf1st  16844  prf2nd  16845  1st2ndprf  16846  curfuncf  16878  curf2ndf  16887  yonedainv  16921  yonffthlem  16922  prdsidlem  17322  pwsco1mhm  17370  pwsco2mhm  17371  frmdup3lem  17403  frmdup3  17404  grpinvcnv  17483  pwsinvg  17528  pwssub  17529  psgnunilem5  17914  efginvrel1  18141  frgpup3lem  18190  frgpup3  18191  gsumval3  18308  gsumcllem  18309  gsumzf1o  18313  gsumzsplit  18327  gsumconst  18334  gsumzmhm  18337  gsumsub  18348  gsum2dlem2  18370  gsumcom2  18374  dprdfadd  18419  dprdfsub  18420  dprdfeq0  18421  dprdf11  18422  dmdprdsplitlem  18436  dprddisj2  18438  dpjidcl  18457  ablfaclem2  18485  ablfac2  18488  mptscmfsuppd  18929  lmhmvsca  19045  rrgsupp  19291  psrbagaddcl  19370  gsumbagdiaglem  19375  psrass1lem  19377  psrlinv  19397  psrass1  19405  psrcom  19409  mplsubrglem  19439  mplmonmul  19464  mplcoe1  19465  mplcoe5  19468  evlslem2  19512  evlslem6  19513  evlslem1  19515  coe1fval3  19578  coe1sclmul  19652  coe1sclmul2  19654  mulgrhm2  19847  cygznlem2a  19916  frgpcyg  19922  uvcresum  20132  frlmup1  20137  grpvrinv  20202  mhmvlin  20203  mdetleib2  20394  mdetralt  20414  mdetunilem9  20426  cayleyhamilton1  20697  neiptopnei  20936  dfac14  21421  ptcnp  21425  lmcn2  21452  cnmpt11f  21467  cnmpt21f  21475  cnmpt2k  21491  qtopeu  21519  xkocnv  21617  xkohmeo  21618  flfcnp2  21811  istgp2  21895  tmdgsum  21899  symgtgp  21905  subgtgp  21909  tgpconncomp  21916  prdstgpd  21928  tsmsmhm  21949  tsmssub  21952  tgptsmscls  21953  tsmssplit  21955  tsmsxplem1  21956  tlmtgp  21999  ustuqtop  22050  prdsmslem1  22332  prdsxmslem1  22333  prdsxmslem2  22334  tngnm  22455  nmoeq0  22540  cnfldnm  22582  cncfmpt1f  22716  negfcncf  22722  cnrehmeo  22752  evth  22758  evth2  22759  copco  22818  pcopt  22822  pcopt2  22823  pcoass  22824  pcorev2  22828  pi1xfrcnv  22857  ovolctb  23258  ovolfs2  23339  uniioombllem2  23351  uniioombllem3  23353  ismbf  23397  mbfconst  23402  ismbfcn2  23406  mbfmulc2re  23415  mbfadd  23428  mbfsub  23429  mbflimsup  23433  itg1climres  23481  mbfi1flimlem  23489  mbfi1flim  23490  mbfmul  23493  itg2uba  23510  itg2mulclem  23513  itg2mulc  23514  itg2splitlem  23515  itg2monolem1  23517  itg2i1fseq  23522  itg2gt0  23527  itg2cnlem1  23528  itg2cnlem2  23529  i1fibl  23574  itgitg1  23575  iblabslem  23594  iblabs  23595  bddmulibl  23605  cnplimc  23651  limccnp  23655  limccnp2  23656  dvcnp2  23683  dvmulf  23706  dvcmulf  23708  dvcobr  23709  dvcof  23711  dvcjbr  23712  dvcj  23713  dvfre  23714  dvmptcj  23731  dvcnvlem  23739  dvcnv  23740  dvef  23743  dvsincos  23744  rolle  23753  cmvth  23754  dvlip  23756  dvlipcn  23757  dv11cn  23764  dvivthlem1  23771  dvivth  23773  lhop2  23778  dvfsumrlim2  23795  ftc1lem1  23798  ftc1lem2  23799  ftc1a  23800  ftc1lem4  23802  ftc2  23807  ftc2ditglem  23808  ftc2ditg  23809  tdeglem4  23820  tdeglem2  23821  mdegle0  23837  mdegmullem  23838  plypf1  23968  plyco  23997  dgrcolem1  24029  dgrcolem2  24030  dgrco  24031  plycjlem  24032  dvply2g  24040  plydiveu  24053  elqaalem3  24076  taylthlem1  24127  taylthlem2  24128  ulmshft  24144  ulmdvlem1  24154  mtest  24158  mtestbdd  24159  mbfulm  24160  iblulm  24161  itgulm  24162  pserulm  24176  pserdv  24183  abelthlem1  24185  abelthlem3  24187  pige3  24269  eff1olem  24294  logcn  24393  advlog  24400  advlogexp  24401  logtayl  24406  logccv  24409  dvcxp1  24481  dvcxp2  24482  dvcncxp1  24484  resqrtcn  24490  sqrtcn  24491  loglesqrt  24499  dvatan  24662  leibpi  24669  divsqrtsumo1  24710  jensenlem2  24714  amgmlem  24716  lgamgulmlem2  24756  lgamcvg2  24781  ftalem7  24805  basellem9  24815  muinv  24919  dchrmulid2  24977  dchrinvcl  24978  lgseisenlem4  25103  dchrisum0lem2a  25206  logdivsum  25222  mulog2sumlem1  25223  log2sumbnd  25233  hilnormi  28020  chscllem4  28499  hmopidmchi  29010  rabfodom  29344  ofoprabco  29464  fpwrelmapffslem  29507  fpwrelmap  29508  qqhre  30064  prodindf  30085  esumpcvgval  30140  ofcfval4  30167  omssubadd  30362  carsggect  30380  plymulx0  30624  fdvneggt  30678  fdvnegge  30680  itgexpif  30684  ptpconn  31215  cvmliftlem6  31272  cvmliftlem8  31274  cvmlift2lem7  31291  cvmliftphtlem  31299  cvmlift3lem5  31305  elmsubrn  31425  knoppcnlem9  32491  curunc  33391  poimir  33442  broucube  33443  mblfinlem2  33447  volsupnfl  33454  cnambfre  33458  dvtan  33460  itg2addnclem  33461  itg2addnclem2  33462  itg2addnclem3  33463  itg2addnc  33464  itg2gt0cn  33465  itgaddnc  33470  itgmulc2nc  33478  bddiblnc  33480  ftc1cnnclem  33483  ftc1anclem1  33485  ftc1anclem2  33486  ftc1anclem3  33487  ftc1anclem4  33488  ftc1anclem5  33489  ftc1anclem6  33490  ftc1anclem7  33491  ftc1anclem8  33492  ftc1anc  33493  ftc2nc  33494  upixp  33524  mzpsubst  37311  diophun  37337  mendlmod  37763  mendassa  37764  fsovcnvlem  38307  binomcxplemnotnn0  38555  rnsnf  39370  cncfmptss  39819  climliminflimsupd  40033  mulcncff  40081  subcncff  40093  cncfcompt  40096  addcncff  40097  divcncff  40104  cncfiooicclem1  40106  dvsinexp  40125  dvsubf  40128  dvdivf  40137  dvcosax  40141  dvnmul  40158  dvnprodlem1  40161  dvnprodlem2  40162  itgsinexplem1  40169  itgsubsticclem  40191  iblcncfioo  40194  itgiccshift  40196  stoweidlem20  40237  dirkercncflem2  40321  fourierdlem16  40340  fourierdlem21  40345  fourierdlem22  40346  fourierdlem28  40352  fourierdlem39  40363  fourierdlem51  40374  fourierdlem60  40383  fourierdlem61  40384  fourierdlem69  40392  fourierdlem72  40395  fourierdlem73  40396  fourierdlem81  40404  fourierdlem83  40406  fourierdlem84  40407  fourierdlem87  40410  fourierdlem90  40413  fourierdlem93  40416  fourierdlem95  40418  fourierdlem101  40424  fourierdlem103  40426  fourierdlem104  40427  fourierdlem111  40434  etransclem34  40485  etransclem43  40494  etransclem46  40497  sge0tsms  40597  sge0fodjrnlem  40633  sge0iun  40636  sge0isum  40644  sge0seq  40663  meadjun  40679  meadjiunlem  40682  meadjiun  40683  ismeannd  40684  psmeasurelem  40687  omeiunle  40731  ovn02  40782  smfpimioo  40994  smfresal  40995  smfinflem  41023  smflimsuplem3  41028  smfliminflem  41036  aacllem  42547  amgmwlem  42548  amgmlemALT  42549