Theorem feqmptd 6953

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ↦ cmpt 5194   Fn wfn 6535  ⟶wf 6536  ‘cfv 6540

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737  ax-sep 5259  ax-nul 5271  ax-pr 5406

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-ral 3082  df-rex 3092  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-opab 5176  df-mpt 5195  df-id 5558  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-iota 6496  df-fun 6542  df-fn 6543  df-f 6544  df-fv 6548

This theorem is used by:  feqresmpt  6954  cofmpt  7132  fcoconst  7134  ofco  7709  caofinvl  7716  caofcom  7721  caofidlcan  7722  caofass  7724  caofdi  7726  caofdir  7727  caonncan  7728  suppssof1  8201  mapxpen  9138  xpmapenlem  9139  cantnfp1  9657  cantnflem1  9665  cnfcom2lem  9677  infxpenc  10018  pwfseqlem5  10663  gruf  10811  ccatco  14896  cnrecnv  15240  rlimclim1  15620  rlimuni  15625  lo1resb  15639  rlimresb  15640  o1resb  15641  rlimcn1  15663  rlimo1  15692  o1rlimmul  15694  caucvgr  15751  ackbijnn  15905  bitsf1ocnv  16524  ramcl  17111  pwsplusgval  17566  pwsmulrval  17567  pwsvscafval  17570  setcepi  18167  prf1st  18282  prf2nd  18283  1st2ndprf  18284  curfuncf  18316  curf2ndf  18325  yonedainv  18359  yonffthlem  18360  prdsidlem  18864  mhmvlin  18896  pwsco1mhm  18928  pwsco2mhm  18929  frmdup3lem  18962  frmdup3  18963  grpinvcnv  19117  pwsinvg  19163  pwssub  19164  efginvrel1  19842  frgpup3lem  19891  frgpup3  19892  gsumval3  20021  gsumcllem  20022  gsumzf1o  20026  gsumzsplit  20041  gsumconst  20048  gsumzmhm  20051  gsumsub  20062  gsum2dlem2  20085  gsumcom2  20089  dprdfadd  20136  dprdfsub  20137  dprdfeq0  20138  dprdf11  20139  dmdprdsplitlem  20153  dprddisj2  20155  dpjidcl  20174  ablfaclem2  20202  ablfac2  20205  rrgsupp  20850  mptscmfsuppd  21099  lmhmvsca  21216  mulgrhm2  21678  cygznlem2a  21767  frgpcyg  21773  uvcresum  21993  frlmup1  21998  gsumbagdiaglem  22131  psrass1lem  22133  psrlinv  22155  psrass1  22163  psrcom  22167  mplsubrglem  22203  mplmonmul  22237  mplcoe1  22238  mplcoe5  22241  evlslem2  22280  evlslem6  22282  evlslem1  22283  selvvvval  22343  mhpmulcl  22362  psdmplcl  22375  psdmul  22379  coe1fval3  22418  coe1sclmul  22493  coe1sclmul2  22495  grpvrinv  22606  mdetleib2  22795  mdetunilem9  22827  cayleyhamilton1  23099  neiptopnei  23339  dfac14  23826  ptcnp  23830  lmcn2  23857  cnmpt11f  23872  cnmpt21f  23880  cnmpt2k  23896  qtopeu  23924  xkocnv  24022  xkohmeo  24023  flfcnp2  24215  istgp2  24299  tmdgsum  24303  subgtgp  24313  symgtgp  24314  tgpconncomp  24321  prdstgpd  24333  tsmssub  24357  tgptsmscls  24358  tsmssplit  24360  tsmsxplem1  24361  tlmtgp  24404  ustuqtop  24454  prdsmslem1  24735  prdsxmslem1  24736  prdsxmslem2  24737  tngnm  24859  nmoeq0  24944  cnfldnm  24986  cncfmpt1f  25124  negfcncf  25133  cnrehmeo  25163  evth  25169  evth2  25170  copco  25228  pcopt  25232  pcopt2  25233  pcoass  25234  pcorev2  25238  pi1xfrcnv  25267  ovolctb  25700  ovolfs2  25781  uniioombllem2  25793  ismbf  25838  mbfconst  25843  mbfmulc2re  25858  mbfadd  25871  mbfsub  25872  mbflimsup  25876  mbfi1flimlem  25932  mbfi1flim  25933  mbfmul  25936  itg2uba  25953  itg2mulclem  25956  itg2mulc  25957  itg2splitlem  25958  itg2monolem1  25960  itg2i1fseq  25965  itg2gt0  25970  itg2cnlem1  25971  itg2cnlem2  25972  i1fibl  26018  itgitg1  26019  bddmulibl  26049  bddiblnc  26052  cnplimc  26097  limccnp2  26102  dvcnp2  26130  dvmulf  26153  dvcmulf  26155  dvcobr  26156  dvcof  26158  dvcj  26160  dvfre  26161  dvmptcj  26178  dvcnvlem  26186  dvcnv  26187  dvef  26190  dvsincos  26191  rolle  26200  cmvth  26201  dvlip  26203  dvlipcn  26204  dv11cn  26211  dvivthlem1  26218  dvivth  26220  lhop2  26225  dvfsumrlim2  26242  ftc1lem1  26245  ftc1lem2  26246  ftc1a  26247  ftc1lem4  26249  ftc2  26254  ftc2ditglem  26255  ftc2ditg  26256  tdeglem4  26268  tdeglem2  26269  mdegle0  26285  mdegmullem  26286  plypf1  26420  plyco  26449  dgrcolem1  26481  dgrcolem2  26482  dgrco  26483  plycjlem  26484  plyn0mulidp  26493  dvply2g  26497  plydiveu  26510  elqaalem3  26533  taylthlem1  26587  taylthlem2  26588  ulmshft  26604  ulmdvlem1  26614  mtest  26618  mtestbdd  26619  mbfulm  26620  iblulm  26621  itgulm  26622  pserulm  26636  pserdv  26643  abelthlem1  26645  abelthlem3  26647  pige3ALT  26736  eff1olem  26764  logcn  26863  advlog  26870  advlogexp  26871  logtayl  26876  logccv  26879  dvcxp1  26956  dvcxp2  26957  dvcncxp1  26959  resqrtcn  26965  sqrtcn  26966  loglesqrt  26977  dvatan  27151  leibpi  27158  divsqrtsumo1  27199  jensenlem2  27203  amgmlem  27205  lgamgulmlem2  27245  ftalem7  27294  basellem9  27304  muinv  27408  dchrmullid  27467  dchrinvcl  27468  dchrisum0lem2a  27732  logdivsum  27748  mulog2sumlem1  27749  log2sumbnd  27759  hilnormi  31586  chscllem4  32063  hmopidmchi  32574  rabfodom  32922  ofoprabco  33080  fpwrelmapffslem  33147  fpwrelmap  33148  prodindf  33252  gsummulsubdishift1  33452  gsumwrd2dccat  33462  elrgspn  33630  elrgspnsubrunlem2  33632  domnprodeq0  33663  deg1prod  33937  selvply1rhmlem2  33975  selvply1rhmlem4  33977  selvply1rhm0  33980  mplmulmvr  33993  evlextv  33996  mplvrpmfgalem  33998  mplvrpmga  33999  mplvrpmrhm  34001  psrgsum  34002  psrmonmul  34004  psrmonprod  34006  issply  34015  esplyfval0  34018  esplyfvaln  34028  lbsdiflsp0  34080  fedgmullem1  34083  extdgfialglem2  34147  qqhre  34474  esumpcvgval  34532  ofcfval4  34559  omssubadd  34755  carsggect  34773  fdvneggt  35052  fdvnegge  35054  itgexpif  35058  ptpconn  35762  cvmliftlem6  35819  cvmliftlem8  35821  cvmlift2lem7  35838  cvmliftphtlem  35846  cvmlift3lem5  35852  elmsubrn  36057  knoppcnlem9  37147  curunc  38310  poimir  38361  broucube  38362  mblfinlem2  38366  volsupnfl  38373  cnambfre  38376  dvtan  38378  itg2addnclem  38379  itg2addnclem2  38380  itg2addnclem3  38381  itg2addnc  38382  itg2gt0cn  38383  itgaddnc  38388  itgmulc2nc  38396  ftc1cnnclem  38399  ftc1anclem1  38401  ftc1anclem2  38402  ftc1anclem3  38403  ftc1anclem4  38404  ftc1anclem5  38405  ftc1anclem6  38406  ftc1anclem7  38407  ftc1anclem8  38408  ftc1anc  38409  ftc2nc  38410  upixp  38438  readvcot  43183  evlselv  43379  fsuppssindlem1  43381  fsuppssindlem2  43382  mhphflem  43386  mhphf  43387  mzpsubst  43537  diophun  43562  mendlmod  43974  mendassa  43975  cantnf2  44110  fsovcnvlem  44797  binomcxplemnotnn0  45124  rnsnf  45960  cncfmptss  46361  climliminflimsupd  46573  mulcncff  46642  subcncff  46652  cncfcompt  46655  addcncff  46656  divcncff  46663  cncfiooicclem1  46665  dvsinexp  46683  dvsubf  46686  dvdivf  46694  dvcosax  46698  dvnmul  46715  dvnprodlem1  46718  dvnprodlem2  46719  itgsinexplem1  46726  itgsubsticclem  46747  iblcncfioo  46750  itgiccshift  46752  stoweidlem20  46792  dirkercncflem2  46876  fourierdlem16  46895  fourierdlem21  46900  fourierdlem22  46901  fourierdlem28  46907  fourierdlem39  46918  fourierdlem51  46929  fourierdlem60  46938  fourierdlem61  46939  fourierdlem69  46947  fourierdlem72  46950  fourierdlem73  46951  fourierdlem81  46959  fourierdlem83  46961  fourierdlem84  46962  fourierdlem87  46965  fourierdlem90  46968  fourierdlem93  46971  fourierdlem95  46973  fourierdlem101  46979  fourierdlem103  46981  fourierdlem104  46982  fourierdlem111  46989  etransclem34  47040  etransclem43  47049  etransclem46  47052  sge0tsms  47152  sge0fodjrnlem  47188  sge0iun  47191  sge0isum  47199  sge0seq  47218  meadjun  47234  meadjiunlem  47237  meadjiun  47238  ismeannd  47239  psmeasurelem  47242  omeiunle  47289  ovn02  47340  smfpimioo  47559  smfresal  47560  smfinflem  47589  smflimsuplem3  47594  smfliminflem  47602  1arymaptfo  49480  diag1  50139  aacllem  50678  amgmwlem  50707  amgmlemALT  50708