Theorem feqmptd 6951

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ↦ cmpt 5186   Fn wfn 6532  ⟶wf 6533  ‘cfv 6537

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 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-sep 5249  ax-nul 5260  ax-pr 5391

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 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-mpt 5187  df-id 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-fv 6545

This theorem is used by:  feqresmpt  6952  cofmpt  7131  fcoconst  7133  ofco  7716  caofinvl  7723  caofcom  7728  caofidlcan  7729  caofass  7731  caofdi  7733  caofdir  7734  caonncan  7735  suppssof1  8209  mapxpen  9155  xpmapenlem  9156  cantnfp1  9675  cantnflem1  9683  cnfcom2lem  9695  infxpenc  10090  pwfseqlem5  10741  gruf  10889  ccatco  14979  cnrecnv  15325  rlimclim1  15705  rlimuni  15710  lo1resb  15724  rlimresb  15725  o1resb  15726  rlimcn1  15748  rlimo1  15777  o1rlimmul  15779  caucvgr  15836  ackbijnn  15990  bitsf1ocnv  16607  ramcl  17200  pwsplusgval  17655  pwsmulrval  17656  pwsvscafval  17659  setcepi  18256  prf1st  18371  prf2nd  18372  1st2ndprf  18373  curfuncf  18405  curf2ndf  18414  yonedainv  18448  yonffthlem  18449  prdsidlem  18956  mhmvlin  18989  pwsco1mhm  19021  pwsco2mhm  19022  frmdup3lem  19055  frmdup3  19056  grpinvcnv  19210  pwsinvg  19256  pwssub  19257  efginvrel1  19935  frgpup3lem  19984  frgpup3  19985  gsumval3  20114  gsumcllem  20115  gsumzf1o  20119  gsumzsplit  20134  gsumconst  20141  gsumzmhm  20144  gsumsub  20155  gsum2dlem2  20178  gsumcom2  20182  dprdfadd  20229  dprdfsub  20230  dprdfeq0  20231  dprdf11  20232  dmdprdsplitlem  20246  dprddisj2  20248  dpjidcl  20267  ablfaclem2  20295  ablfac2  20298  rrgsupp  20946  mptscmfsuppd  21196  lmhmvsca  21313  mulgrhm2  21777  cygznlem2a  21866  frgpcyg  21872  uvcresum  22092  frlmup1  22097  gsumbagdiaglem  22232  psrass1lem  22234  psrlinv  22256  psrass1  22264  psrcom  22268  mplsubrglem  22304  mplmonmul  22338  mplcoe1  22339  mplcoe5  22342  evlslem2  22381  evlslem6  22383  evlslem1  22384  selvvvval  22444  mhpmulcl  22463  psdmplcl  22476  psdmul  22480  coe1fval3  22519  coe1sclmul  22594  coe1sclmul2  22596  grpvrinv  22707  mdetleib2  22896  mdetunilem9  22928  cayleyhamilton1  23203  neiptopnei  23443  dfac14  23930  ptcnp  23934  lmcn2  23961  cnmpt11f  23976  cnmpt21f  23984  cnmpt2k  24000  qtopeu  24028  xkocnv  24126  xkohmeo  24127  flfcnp2  24319  istgp2  24403  tmdgsum  24407  subgtgp  24417  symgtgp  24418  tgpconncomp  24425  prdstgpd  24437  tsmssub  24461  tgptsmscls  24462  tsmssplit  24464  tsmsxplem1  24465  tlmtgp  24508  ustuqtop  24558  prdsmslem1  24839  prdsxmslem1  24840  prdsxmslem2  24841  tngnm  24963  nmoeq0  25048  cnfldnm  25090  cncfmpt1f  25228  negfcncf  25237  cnrehmeo  25267  evth  25273  evth2  25274  copco  25332  pcopt  25336  pcopt2  25337  pcoass  25338  pcorev2  25342  pi1xfrcnv  25371  ovolctb  25804  ovolfs2  25885  uniioombllem2  25897  ismbf  25942  mbfconst  25947  mbfmulc2re  25962  mbfadd  25975  mbfsub  25976  mbflimsup  25980  mbfi1flimlem  26036  mbfi1flim  26037  mbfmul  26040  itg2uba  26057  itg2mulclem  26060  itg2mulc  26061  itg2splitlem  26062  itg2monolem1  26064  itg2i1fseq  26069  itg2gt0  26074  itg2cnlem1  26075  itg2cnlem2  26076  i1fibl  26121  itgitg1  26122  bddmulibl  26152  bddiblnc  26155  cnplimc  26200  limccnp2  26205  dvcnp2  26233  dvmulf  26256  dvcmulf  26258  dvcobr  26259  dvcof  26261  dvcj  26263  dvfre  26264  dvmptcj  26281  dvcnvlem  26289  dvcnv  26290  dvef  26293  dvsincos  26294  rolle  26303  cmvth  26304  dvlip  26306  dvlipcn  26307  dv11cn  26314  dvivthlem1  26321  dvivth  26323  lhop2  26328  dvfsumrlim2  26345  ftc1lem1  26348  ftc1lem2  26349  ftc1a  26350  ftc1lem4  26352  ftc2  26357  ftc2ditglem  26358  ftc2ditg  26359  tdeglem4  26371  tdeglem2  26372  mdegle0  26388  mdegmullem  26389  plypf1  26524  plyco  26553  dgrcolem1  26585  dgrcolem2  26586  dgrco  26587  plycjlem  26588  plyn0mulidp  26595  dvply2g  26599  plydiveu  26612  elqaalem3  26637  taylthlem1  26693  taylthlem2  26694  ulmshft  26710  ulmdvlem1  26720  mtest  26724  mtestbdd  26725  mbfulm  26726  iblulm  26727  itgulm  26728  pserulm  26742  pserdv  26749  abelthlem1  26751  abelthlem3  26753  pige3ALT  26841  eff1olem  26869  logcn  26968  advlog  26975  advlogexp  26976  logtayl  26981  logccv  26984  dvcxp1  27061  dvcxp2  27062  dvcncxp1  27064  resqrtcn  27070  sqrtcn  27071  loglesqrt  27082  dvatan  27256  leibpi  27263  divsqrtsumo1  27304  jensenlem2  27308  amgmlem  27310  lgamgulmlem2  27350  ftalem7  27399  basellem9  27409  muinv  27513  dchrmullid  27572  dchrinvcl  27573  dchrisum0lem2a  27837  logdivsum  27853  mulog2sumlem1  27854  log2sumbnd  27864  hilnormi  31758  chscllem4  32235  hmopidmchi  32746  rabfodom  33094  ofoprabco  33251  fpwrelmapffslem  33317  fpwrelmap  33318  prodindf  33422  gsummulsubdishift1  33622  gsumwrd2dccat  33632  elrgspn  33800  elrgspnsubrunlem2  33802  domnprodeq0  33833  deg1prod  34108  selvply1rhmlem2  34146  selvply1rhmlem4  34148  selvply1rhm0  34151  mplmulmvr  34164  evlextv  34167  mplvrpmfgalem  34169  mplvrpmga  34170  mplvrpmrhm  34172  psrgsum  34173  psrmonmul  34175  psrmonprod  34177  issply  34186  esplyfval0  34189  esplyfvaln  34199  lbsdiflsp0  34251  fedgmullem1  34254  extdgfialglem2  34318  qqhre  34645  esumpcvgval  34703  ofcfval4  34730  omssubadd  34925  carsggect  34943  fdvneggt  35222  fdvnegge  35224  itgexpif  35228  ptpconn  35977  cvmliftlem6  36034  cvmliftlem8  36036  cvmlift2lem7  36053  cvmliftphtlem  36061  cvmlift3lem5  36067  elmsubrn  36272  knoppcnlem9  37347  curunc  38505  poimir  38551  broucube  38552  mblfinlem2  38556  volsupnfl  38563  cnambfre  38566  dvtan  38568  itg2addnclem  38569  itg2addnclem2  38570  itg2addnclem3  38571  itg2addnc  38572  itg2gt0cn  38573  itgaddnc  38578  itgmulc2nc  38586  ftc1cnnclem  38589  ftc1anclem1  38591  ftc1anclem2  38592  ftc1anclem3  38593  ftc1anclem4  38594  ftc1anclem5  38595  ftc1anclem6  38596  ftc1anclem7  38597  ftc1anclem8  38598  ftc1anc  38599  ftc2nc  38600  upixp  38643  readvcot  43395  evlselv  43597  fsuppssindlem1  43599  fsuppssindlem2  43600  mhphflem  43604  mhphf  43605  mzpsubst  43738  diophun  43763  mendlmod  44175  mendassa  44176  cantnf2  44311  fsovcnvlem  44998  binomcxplemnotnn0  45325  rnsnf  46168  cncfmptss  46568  climliminflimsupd  46780  mulcncff  46849  subcncff  46859  cncfcompt  46862  addcncff  46863  divcncff  46870  cncfiooicclem1  46872  dvsinexp  46890  dvsubf  46893  dvdivf  46901  dvcosax  46905  dvnmul  46922  dvnprodlem1  46925  dvnprodlem2  46926  itgsinexplem1  46933  itgsubsticclem  46954  iblcncfioo  46957  itgiccshift  46959  stoweidlem20  46999  dirkercncflem2  47083  fourierdlem16  47102  fourierdlem21  47107  fourierdlem22  47108  fourierdlem28  47114  fourierdlem39  47125  fourierdlem51  47136  fourierdlem60  47145  fourierdlem61  47146  fourierdlem69  47154  fourierdlem72  47157  fourierdlem73  47158  fourierdlem81  47166  fourierdlem83  47168  fourierdlem84  47169  fourierdlem87  47172  fourierdlem90  47175  fourierdlem93  47178  fourierdlem95  47180  fourierdlem101  47186  fourierdlem103  47188  fourierdlem104  47189  fourierdlem111  47196  etransclem34  47247  etransclem43  47256  etransclem46  47259  sge0tsms  47359  sge0fodjrnlem  47395  sge0iun  47398  sge0isum  47406  sge0seq  47425  meadjun  47441  meadjiunlem  47444  meadjiun  47445  ismeannd  47446  psmeasurelem  47449  omeiunle  47496  ovn02  47547  smfpimioo  47766  smfresal  47767  smfinflem  47796  smflimsuplem3  47801  smfliminflem  47809  1arymaptfo  49724  diag1  50381  dvsec  50825  dvcsc  50826  dvcot  50827  aacllem  50908  amgmwlem  50956  amgmlemALT  50957