Theorem feqmptd 6885

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

Hypothesis

Ref	Expression
feqmptd.1	⊢ (𝜑 → 𝐹:𝐴⟶𝐵)

Assertion

Ref	Expression
feqmptd	⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)))

Distinct variable groups:   𝑥,𝐴   𝑥,𝐹

Allowed substitution hints:   𝜑(𝑥)   𝐵(𝑥)

Proof of Theorem feqmptd

Step	Hyp	Ref	Expression
1		feqmptd.1	. . 3 ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)
2	1	ffnd 6647	. 2 ⊢ (𝜑 → 𝐹 Fn 𝐴)
3		dffn5 6875	. 2 ⊢ (𝐹 Fn 𝐴 ↔ 𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)))
4	2, 3	sylib 218	1 ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)))

Syntax hints:   → wi 4   = wceq 1541   ↦ cmpt 5167   Fn wfn 6471  ⟶wf 6472  ‘cfv 6476

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-sep 5229  ax-nul 5239  ax-pr 5365

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ne 2929  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-ss 3914  df-nul 4279  df-if 4471  df-sn 4572  df-pr 4574  df-op 4578  df-uni 4855  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5506  df-xp 5617  df-rel 5618  df-cnv 5619  df-co 5620  df-dm 5621  df-iota 6432  df-fun 6478  df-fn 6479  df-f 6480  df-fv 6484

This theorem is referenced by:  feqresmpt  6886  cofmpt  7060  fcoconst  7062  ofco  7630  caofinvl  7637  caofcom  7642  caofidlcan  7643  caofass  7645  caofdi  7647  caofdir  7648  caonncan  7649  suppssof1  8124  mapxpen  9051  xpmapenlem  9052  cantnfp1  9566  cantnflem1  9574  cnfcom2lem  9586  infxpenc  9904  pwfseqlem5  10549  gruf  10697  ccatco  14737  cnrecnv  15067  rlimclim1  15447  rlimuni  15452  lo1resb  15466  rlimresb  15467  o1resb  15468  rlimcn1  15490  rlimo1  15519  o1rlimmul  15521  caucvgr  15578  ackbijnn  15730  bitsf1ocnv  16350  ramcl  16936  pwsplusgval  17389  pwsmulrval  17390  pwsvscafval  17393  setcepi  17990  prf1st  18105  prf2nd  18106  1st2ndprf  18107  curfuncf  18139  curf2ndf  18148  yonedainv  18182  yonffthlem  18183  prdsidlem  18672  mhmvlin  18704  pwsco1mhm  18735  pwsco2mhm  18736  frmdup3lem  18769  frmdup3  18770  grpinvcnv  18914  pwsinvg  18961  pwssub  18962  efginvrel1  19635  frgpup3lem  19684  frgpup3  19685  gsumval3  19814  gsumcllem  19815  gsumzf1o  19819  gsumzsplit  19834  gsumconst  19841  gsumzmhm  19844  gsumsub  19855  gsum2dlem2  19878  gsumcom2  19882  dprdfadd  19929  dprdfsub  19930  dprdfeq0  19931  dprdf11  19932  dmdprdsplitlem  19946  dprddisj2  19948  dpjidcl  19967  ablfaclem2  19995  ablfac2  19998  rrgsupp  20611  mptscmfsuppd  20856  lmhmvsca  20974  mulgrhm2  21410  cygznlem2a  21499  frgpcyg  21505  uvcresum  21725  frlmup1  21730  gsumbagdiaglem  21862  psrass1lem  21864  psrlinv  21887  psrass1  21896  psrcom  21900  mplsubrglem  21936  mplmonmul  21966  mplcoe1  21967  mplcoe5  21970  evlslem2  22009  evlslem6  22011  evlslem1  22012  mhpmulcl  22059  psdmplcl  22072  psdmul  22076  coe1fval3  22116  coe1sclmul  22191  coe1sclmul2  22193  grpvrinv  22309  mdetleib2  22498  mdetunilem9  22530  cayleyhamilton1  22802  neiptopnei  23042  dfac14  23528  ptcnp  23532  lmcn2  23559  cnmpt11f  23574  cnmpt21f  23582  cnmpt2k  23598  qtopeu  23626  xkocnv  23724  xkohmeo  23725  flfcnp2  23917  istgp2  24001  tmdgsum  24005  subgtgp  24015  symgtgp  24016  tgpconncomp  24023  prdstgpd  24035  tsmssub  24059  tgptsmscls  24060  tsmssplit  24062  tsmsxplem1  24063  tlmtgp  24106  ustuqtop  24156  prdsmslem1  24437  prdsxmslem1  24438  prdsxmslem2  24439  tngnm  24561  nmoeq0  24646  cnfldnm  24688  cncfmpt1f  24829  negfcncf  24839  cnrehmeo  24873  cnrehmeoOLD  24874  evth  24880  evth2  24881  copco  24940  pcopt  24944  pcopt2  24945  pcoass  24946  pcorev2  24950  pi1xfrcnv  24979  ovolctb  25413  ovolfs2  25494  uniioombllem2  25506  ismbf  25551  mbfconst  25556  mbfmulc2re  25571  mbfadd  25584  mbfsub  25585  mbflimsup  25589  mbfi1flimlem  25645  mbfi1flim  25646  mbfmul  25649  itg2uba  25666  itg2mulclem  25669  itg2mulc  25670  itg2splitlem  25671  itg2monolem1  25673  itg2i1fseq  25678  itg2gt0  25683  itg2cnlem1  25684  itg2cnlem2  25685  i1fibl  25731  itgitg1  25732  bddmulibl  25762  bddiblnc  25765  cnplimc  25810  limccnp2  25815  dvcnp2  25843  dvcnp2OLD  25844  dvmulf  25868  dvcmulf  25870  dvcobr  25871  dvcobrOLD  25872  dvcof  25874  dvcj  25876  dvfre  25877  dvmptcj  25894  dvcnvlem  25902  dvcnv  25903  dvef  25906  dvsincos  25907  rolle  25916  cmvth  25917  cmvthOLD  25918  dvlip  25920  dvlipcn  25921  dv11cn  25928  dvivthlem1  25935  dvivth  25937  lhop2  25942  dvfsumrlim2  25961  ftc1lem1  25964  ftc1lem2  25965  ftc1a  25966  ftc1lem4  25968  ftc2  25973  ftc2ditglem  25974  ftc2ditg  25975  tdeglem4  25987  tdeglem2  25988  mdegle0  26004  mdegmullem  26005  plypf1  26139  plyco  26168  dgrcolem1  26201  dgrcolem2  26202  dgrco  26203  plycjlem  26204  dvply2g  26214  dvply2gOLD  26215  plydiveu  26228  elqaalem3  26251  taylthlem1  26303  taylthlem2  26304  taylthlem2OLD  26305  ulmshft  26321  ulmdvlem1  26331  mtest  26335  mtestbdd  26336  mbfulm  26337  iblulm  26338  itgulm  26339  pserulm  26353  pserdv  26361  abelthlem1  26363  abelthlem3  26365  pige3ALT  26451  eff1olem  26479  logcn  26578  advlog  26585  advlogexp  26586  logtayl  26591  logccv  26594  dvcxp1  26671  dvcxp2  26672  dvcncxp1  26674  resqrtcn  26681  sqrtcn  26682  loglesqrt  26693  dvatan  26867  leibpi  26874  divsqrtsumo1  26916  jensenlem2  26920  amgmlem  26922  lgamgulmlem2  26962  ftalem7  27011  basellem9  27021  muinv  27125  dchrmullid  27185  dchrinvcl  27186  dchrisum0lem2a  27450  logdivsum  27466  mulog2sumlem1  27467  log2sumbnd  27477  hilnormi  31135  chscllem4  31612  hmopidmchi  32123  rabfodom  32477  ofoprabco  32638  fpwrelmapffslem  32707  fpwrelmap  32708  prodindf  32836  gsumwrd2dccat  33039  elrgspn  33205  elrgspnsubrunlem2  33207  mplvrpmfgalem  33566  mplvrpmga  33567  mplvrpmrhm  33569  issply  33576  lbsdiflsp0  33631  fedgmullem1  33634  extdgfialglem2  33698  qqhre  34025  esumpcvgval  34083  ofcfval4  34110  omssubadd  34305  carsggect  34323  plymulx0  34552  fdvneggt  34605  fdvnegge  34607  itgexpif  34611  ptpconn  35269  cvmliftlem6  35326  cvmliftlem8  35328  cvmlift2lem7  35345  cvmliftphtlem  35353  cvmlift3lem5  35359  elmsubrn  35564  knoppcnlem9  36535  curunc  37642  poimir  37693  broucube  37694  mblfinlem2  37698  volsupnfl  37705  cnambfre  37708  dvtan  37710  itg2addnclem  37711  itg2addnclem2  37712  itg2addnclem3  37713  itg2addnc  37714  itg2gt0cn  37715  itgaddnc  37720  itgmulc2nc  37728  ftc1cnnclem  37731  ftc1anclem1  37733  ftc1anclem2  37734  ftc1anclem3  37735  ftc1anclem4  37736  ftc1anclem5  37737  ftc1anclem6  37738  ftc1anclem7  37739  ftc1anclem8  37740  ftc1anc  37741  ftc2nc  37742  upixp  37769  readvcot  42397  selvvvval  42618  evlselv  42620  fsuppssindlem1  42624  fsuppssindlem2  42625  mhphflem  42629  mhphf  42630  mzpsubst  42781  diophun  42806  mendlmod  43222  mendassa  43223  cantnf2  43358  fsovcnvlem  44046  binomcxplemnotnn0  44389  rnsnf  45221  cncfmptss  45627  climliminflimsupd  45839  mulcncff  45908  subcncff  45918  cncfcompt  45921  addcncff  45922  divcncff  45929  cncfiooicclem1  45931  dvsinexp  45949  dvsubf  45952  dvdivf  45960  dvcosax  45964  dvnmul  45981  dvnprodlem1  45984  dvnprodlem2  45985  itgsinexplem1  45992  itgsubsticclem  46013  iblcncfioo  46016  itgiccshift  46018  stoweidlem20  46058  dirkercncflem2  46142  fourierdlem16  46161  fourierdlem21  46166  fourierdlem22  46167  fourierdlem28  46173  fourierdlem39  46184  fourierdlem51  46195  fourierdlem60  46204  fourierdlem61  46205  fourierdlem69  46213  fourierdlem72  46216  fourierdlem73  46217  fourierdlem81  46225  fourierdlem83  46227  fourierdlem84  46228  fourierdlem87  46231  fourierdlem90  46234  fourierdlem93  46237  fourierdlem95  46239  fourierdlem101  46245  fourierdlem103  46247  fourierdlem104  46248  fourierdlem111  46255  etransclem34  46306  etransclem43  46315  etransclem46  46318  sge0tsms  46418  sge0fodjrnlem  46454  sge0iun  46457  sge0isum  46465  sge0seq  46484  meadjun  46500  meadjiunlem  46503  meadjiun  46504  ismeannd  46505  psmeasurelem  46508  omeiunle  46555  ovn02  46606  smfpimioo  46825  smfresal  46826  smfinflem  46855  smflimsuplem3  46860  smfliminflem  46868  1arymaptfo  48675  diag1  49336  aacllem  49833  amgmwlem  49834  amgmlemALT  49835