Theorem feqmptd 6910

Description: Deduction form of dffn5 6900. (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 6671	. 2 ⊢ (𝜑 → 𝐹 Fn 𝐴)
3		dffn5 6900	. 2 ⊢ (𝐹 Fn 𝐴 ↔ 𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)))
4	2, 3	sylib 218	1 ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)))

Syntax hints:   → wi 4   = wceq 1542   ↦ cmpt 5181   Fn wfn 6495  ⟶wf 6496  ‘cfv 6500

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5243  ax-nul 5253  ax-pr 5379

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5527  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-iota 6456  df-fun 6502  df-fn 6503  df-f 6504  df-fv 6508

This theorem is referenced by:  feqresmpt  6911  cofmpt  7087  fcoconst  7089  ofco  7657  caofinvl  7664  caofcom  7669  caofidlcan  7670  caofass  7672  caofdi  7674  caofdir  7675  caonncan  7676  suppssof1  8151  mapxpen  9083  xpmapenlem  9084  cantnfp1  9602  cantnflem1  9610  cnfcom2lem  9622  infxpenc  9940  pwfseqlem5  10586  gruf  10734  ccatco  14770  cnrecnv  15100  rlimclim1  15480  rlimuni  15485  lo1resb  15499  rlimresb  15500  o1resb  15501  rlimcn1  15523  rlimo1  15552  o1rlimmul  15554  caucvgr  15611  ackbijnn  15763  bitsf1ocnv  16383  ramcl  16969  pwsplusgval  17423  pwsmulrval  17424  pwsvscafval  17427  setcepi  18024  prf1st  18139  prf2nd  18140  1st2ndprf  18141  curfuncf  18173  curf2ndf  18182  yonedainv  18216  yonffthlem  18217  prdsidlem  18706  mhmvlin  18738  pwsco1mhm  18769  pwsco2mhm  18770  frmdup3lem  18803  frmdup3  18804  grpinvcnv  18948  pwsinvg  18995  pwssub  18996  efginvrel1  19669  frgpup3lem  19718  frgpup3  19719  gsumval3  19848  gsumcllem  19849  gsumzf1o  19853  gsumzsplit  19868  gsumconst  19875  gsumzmhm  19878  gsumsub  19889  gsum2dlem2  19912  gsumcom2  19916  dprdfadd  19963  dprdfsub  19964  dprdfeq0  19965  dprdf11  19966  dmdprdsplitlem  19980  dprddisj2  19982  dpjidcl  20001  ablfaclem2  20029  ablfac2  20032  rrgsupp  20646  mptscmfsuppd  20891  lmhmvsca  21009  mulgrhm2  21445  cygznlem2a  21534  frgpcyg  21540  uvcresum  21760  frlmup1  21765  gsumbagdiaglem  21898  psrass1lem  21900  psrlinv  21923  psrass1  21931  psrcom  21935  mplsubrglem  21971  mplmonmul  22003  mplcoe1  22004  mplcoe5  22007  evlslem2  22046  evlslem6  22048  evlslem1  22049  mhpmulcl  22104  psdmplcl  22117  psdmul  22121  coe1fval3  22161  coe1sclmul  22236  coe1sclmul2  22238  grpvrinv  22355  mdetleib2  22544  mdetunilem9  22576  cayleyhamilton1  22848  neiptopnei  23088  dfac14  23574  ptcnp  23578  lmcn2  23605  cnmpt11f  23620  cnmpt21f  23628  cnmpt2k  23644  qtopeu  23672  xkocnv  23770  xkohmeo  23771  flfcnp2  23963  istgp2  24047  tmdgsum  24051  subgtgp  24061  symgtgp  24062  tgpconncomp  24069  prdstgpd  24081  tsmssub  24105  tgptsmscls  24106  tsmssplit  24108  tsmsxplem1  24109  tlmtgp  24152  ustuqtop  24202  prdsmslem1  24483  prdsxmslem1  24484  prdsxmslem2  24485  tngnm  24607  nmoeq0  24692  cnfldnm  24734  cncfmpt1f  24875  negfcncf  24885  cnrehmeo  24919  cnrehmeoOLD  24920  evth  24926  evth2  24927  copco  24986  pcopt  24990  pcopt2  24991  pcoass  24992  pcorev2  24996  pi1xfrcnv  25025  ovolctb  25459  ovolfs2  25540  uniioombllem2  25552  ismbf  25597  mbfconst  25602  mbfmulc2re  25617  mbfadd  25630  mbfsub  25631  mbflimsup  25635  mbfi1flimlem  25691  mbfi1flim  25692  mbfmul  25695  itg2uba  25712  itg2mulclem  25715  itg2mulc  25716  itg2splitlem  25717  itg2monolem1  25719  itg2i1fseq  25724  itg2gt0  25729  itg2cnlem1  25730  itg2cnlem2  25731  i1fibl  25777  itgitg1  25778  bddmulibl  25808  bddiblnc  25811  cnplimc  25856  limccnp2  25861  dvcnp2  25889  dvcnp2OLD  25890  dvmulf  25914  dvcmulf  25916  dvcobr  25917  dvcobrOLD  25918  dvcof  25920  dvcj  25922  dvfre  25923  dvmptcj  25940  dvcnvlem  25948  dvcnv  25949  dvef  25952  dvsincos  25953  rolle  25962  cmvth  25963  cmvthOLD  25964  dvlip  25966  dvlipcn  25967  dv11cn  25974  dvivthlem1  25981  dvivth  25983  lhop2  25988  dvfsumrlim2  26007  ftc1lem1  26010  ftc1lem2  26011  ftc1a  26012  ftc1lem4  26014  ftc2  26019  ftc2ditglem  26020  ftc2ditg  26021  tdeglem4  26033  tdeglem2  26034  mdegle0  26050  mdegmullem  26051  plypf1  26185  plyco  26214  dgrcolem1  26247  dgrcolem2  26248  dgrco  26249  plycjlem  26250  dvply2g  26260  dvply2gOLD  26261  plydiveu  26274  elqaalem3  26297  taylthlem1  26349  taylthlem2  26350  taylthlem2OLD  26351  ulmshft  26367  ulmdvlem1  26377  mtest  26381  mtestbdd  26382  mbfulm  26383  iblulm  26384  itgulm  26385  pserulm  26399  pserdv  26407  abelthlem1  26409  abelthlem3  26411  pige3ALT  26497  eff1olem  26525  logcn  26624  advlog  26631  advlogexp  26632  logtayl  26637  logccv  26640  dvcxp1  26717  dvcxp2  26718  dvcncxp1  26720  resqrtcn  26727  sqrtcn  26728  loglesqrt  26739  dvatan  26913  leibpi  26920  divsqrtsumo1  26962  jensenlem2  26966  amgmlem  26968  lgamgulmlem2  27008  ftalem7  27057  basellem9  27067  muinv  27171  dchrmullid  27231  dchrinvcl  27232  dchrisum0lem2a  27496  logdivsum  27512  mulog2sumlem1  27513  log2sumbnd  27523  hilnormi  31251  chscllem4  31728  hmopidmchi  32239  rabfodom  32592  ofoprabco  32754  fpwrelmapffslem  32822  fpwrelmap  32823  prodindf  32955  gsummulsubdishift1  33162  gsumwrd2dccat  33172  elrgspn  33340  elrgspnsubrunlem2  33342  domnprodeq0  33370  deg1prod  33676  mplmulmvr  33716  evlextv  33719  mplvrpmfgalem  33721  mplvrpmga  33722  mplvrpmrhm  33724  psrgsum  33725  psrmonmul  33727  psrmonprod  33729  issply  33738  esplyfval0  33741  esplyfvaln  33751  lbsdiflsp0  33804  fedgmullem1  33807  extdgfialglem2  33871  qqhre  34198  esumpcvgval  34256  ofcfval4  34283  omssubadd  34478  carsggect  34496  plymulx0  34725  fdvneggt  34778  fdvnegge  34780  itgexpif  34784  ptpconn  35449  cvmliftlem6  35506  cvmliftlem8  35508  cvmlift2lem7  35525  cvmliftphtlem  35533  cvmlift3lem5  35539  elmsubrn  35744  knoppcnlem9  36723  curunc  37853  poimir  37904  broucube  37905  mblfinlem2  37909  volsupnfl  37916  cnambfre  37919  dvtan  37921  itg2addnclem  37922  itg2addnclem2  37923  itg2addnclem3  37924  itg2addnc  37925  itg2gt0cn  37926  itgaddnc  37931  itgmulc2nc  37939  ftc1cnnclem  37942  ftc1anclem1  37944  ftc1anclem2  37945  ftc1anclem3  37946  ftc1anclem4  37947  ftc1anclem5  37948  ftc1anclem6  37949  ftc1anclem7  37950  ftc1anclem8  37951  ftc1anc  37952  ftc2nc  37953  upixp  37980  readvcot  42734  selvvvval  42943  evlselv  42945  fsuppssindlem1  42949  fsuppssindlem2  42950  mhphflem  42954  mhphf  42955  mzpsubst  43105  diophun  43130  mendlmod  43546  mendassa  43547  cantnf2  43682  fsovcnvlem  44369  binomcxplemnotnn0  44712  rnsnf  45543  cncfmptss  45947  climliminflimsupd  46159  mulcncff  46228  subcncff  46238  cncfcompt  46241  addcncff  46242  divcncff  46249  cncfiooicclem1  46251  dvsinexp  46269  dvsubf  46272  dvdivf  46280  dvcosax  46284  dvnmul  46301  dvnprodlem1  46304  dvnprodlem2  46305  itgsinexplem1  46312  itgsubsticclem  46333  iblcncfioo  46336  itgiccshift  46338  stoweidlem20  46378  dirkercncflem2  46462  fourierdlem16  46481  fourierdlem21  46486  fourierdlem22  46487  fourierdlem28  46493  fourierdlem39  46504  fourierdlem51  46515  fourierdlem60  46524  fourierdlem61  46525  fourierdlem69  46533  fourierdlem72  46536  fourierdlem73  46537  fourierdlem81  46545  fourierdlem83  46547  fourierdlem84  46548  fourierdlem87  46551  fourierdlem90  46554  fourierdlem93  46557  fourierdlem95  46559  fourierdlem101  46565  fourierdlem103  46567  fourierdlem104  46568  fourierdlem111  46575  etransclem34  46626  etransclem43  46635  etransclem46  46638  sge0tsms  46738  sge0fodjrnlem  46774  sge0iun  46777  sge0isum  46785  sge0seq  46804  meadjun  46820  meadjiunlem  46823  meadjiun  46824  ismeannd  46825  psmeasurelem  46828  omeiunle  46875  ovn02  46926  smfpimioo  47145  smfresal  47146  smfinflem  47175  smflimsuplem3  47180  smfliminflem  47188  1arymaptfo  49003  diag1  49663  aacllem  50160  amgmwlem  50161  amgmlemALT  50162