Theorem feqmptd 6946

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

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

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 2732  ax-sep 5251  ax-nul 5263  ax-pr 5398

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 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  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 5550  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-iota 6489  df-fun 6535  df-fn 6536  df-f 6537  df-fv 6541

This theorem is used by:  feqresmpt  6947  cofmpt  7126  fcoconst  7128  ofco  7703  caofinvl  7710  caofcom  7715  caofidlcan  7716  caofass  7718  caofdi  7720  caofdir  7721  caonncan  7722  suppssof1  8197  mapxpen  9141  xpmapenlem  9142  cantnfp1  9660  cantnflem1  9668  cnfcom2lem  9680  infxpenc  10021  pwfseqlem5  10672  gruf  10820  ccatco  14906  cnrecnv  15252  rlimclim1  15632  rlimuni  15637  lo1resb  15651  rlimresb  15652  o1resb  15653  rlimcn1  15675  rlimo1  15704  o1rlimmul  15706  caucvgr  15763  ackbijnn  15917  bitsf1ocnv  16534  ramcl  17121  pwsplusgval  17576  pwsmulrval  17577  pwsvscafval  17580  setcepi  18177  prf1st  18292  prf2nd  18293  1st2ndprf  18294  curfuncf  18326  curf2ndf  18335  yonedainv  18369  yonffthlem  18370  prdsidlem  18876  mhmvlin  18909  pwsco1mhm  18941  pwsco2mhm  18942  frmdup3lem  18975  frmdup3  18976  grpinvcnv  19130  pwsinvg  19176  pwssub  19177  efginvrel1  19855  frgpup3lem  19904  frgpup3  19905  gsumval3  20034  gsumcllem  20035  gsumzf1o  20039  gsumzsplit  20054  gsumconst  20061  gsumzmhm  20064  gsumsub  20075  gsum2dlem2  20098  gsumcom2  20102  dprdfadd  20149  dprdfsub  20150  dprdfeq0  20151  dprdf11  20152  dmdprdsplitlem  20166  dprddisj2  20168  dpjidcl  20187  ablfaclem2  20215  ablfac2  20218  rrgsupp  20863  mptscmfsuppd  21112  lmhmvsca  21229  mulgrhm2  21691  cygznlem2a  21780  frgpcyg  21786  uvcresum  22006  frlmup1  22011  gsumbagdiaglem  22146  psrass1lem  22148  psrlinv  22170  psrass1  22178  psrcom  22182  mplsubrglem  22218  mplmonmul  22252  mplcoe1  22253  mplcoe5  22256  evlslem2  22295  evlslem6  22297  evlslem1  22298  selvvvval  22358  mhpmulcl  22377  psdmplcl  22390  psdmul  22394  coe1fval3  22433  coe1sclmul  22508  coe1sclmul2  22510  grpvrinv  22621  mdetleib2  22810  mdetunilem9  22842  cayleyhamilton1  23117  neiptopnei  23357  dfac14  23844  ptcnp  23848  lmcn2  23875  cnmpt11f  23890  cnmpt21f  23898  cnmpt2k  23914  qtopeu  23942  xkocnv  24040  xkohmeo  24041  flfcnp2  24233  istgp2  24317  tmdgsum  24321  subgtgp  24331  symgtgp  24332  tgpconncomp  24339  prdstgpd  24351  tsmssub  24375  tgptsmscls  24376  tsmssplit  24378  tsmsxplem1  24379  tlmtgp  24422  ustuqtop  24472  prdsmslem1  24753  prdsxmslem1  24754  prdsxmslem2  24755  tngnm  24877  nmoeq0  24962  cnfldnm  25004  cncfmpt1f  25142  negfcncf  25151  cnrehmeo  25181  evth  25187  evth2  25188  copco  25246  pcopt  25250  pcopt2  25251  pcoass  25252  pcorev2  25256  pi1xfrcnv  25285  ovolctb  25718  ovolfs2  25799  uniioombllem2  25811  ismbf  25856  mbfconst  25861  mbfmulc2re  25876  mbfadd  25889  mbfsub  25890  mbflimsup  25894  mbfi1flimlem  25950  mbfi1flim  25951  mbfmul  25954  itg2uba  25971  itg2mulclem  25974  itg2mulc  25975  itg2splitlem  25976  itg2monolem1  25978  itg2i1fseq  25983  itg2gt0  25988  itg2cnlem1  25989  itg2cnlem2  25990  i1fibl  26035  itgitg1  26036  bddmulibl  26066  bddiblnc  26069  cnplimc  26114  limccnp2  26119  dvcnp2  26147  dvmulf  26170  dvcmulf  26172  dvcobr  26173  dvcof  26175  dvcj  26177  dvfre  26178  dvmptcj  26195  dvcnvlem  26203  dvcnv  26204  dvef  26207  dvsincos  26208  rolle  26217  cmvth  26218  dvlip  26220  dvlipcn  26221  dv11cn  26228  dvivthlem1  26235  dvivth  26237  lhop2  26242  dvfsumrlim2  26259  ftc1lem1  26262  ftc1lem2  26263  ftc1a  26264  ftc1lem4  26266  ftc2  26271  ftc2ditglem  26272  ftc2ditg  26273  tdeglem4  26285  tdeglem2  26286  mdegle0  26302  mdegmullem  26303  plypf1  26438  plyco  26467  dgrcolem1  26499  dgrcolem2  26500  dgrco  26501  plycjlem  26502  plyn0mulidp  26511  dvply2g  26515  plydiveu  26528  elqaalem3  26553  taylthlem1  26609  taylthlem2  26610  ulmshft  26626  ulmdvlem1  26636  mtest  26640  mtestbdd  26641  mbfulm  26642  iblulm  26643  itgulm  26644  pserulm  26658  pserdv  26665  abelthlem1  26667  abelthlem3  26669  pige3ALT  26757  eff1olem  26785  logcn  26884  advlog  26891  advlogexp  26892  logtayl  26897  logccv  26900  dvcxp1  26977  dvcxp2  26978  dvcncxp1  26980  resqrtcn  26986  sqrtcn  26987  loglesqrt  26998  dvatan  27172  leibpi  27179  divsqrtsumo1  27220  jensenlem2  27224  amgmlem  27226  lgamgulmlem2  27266  ftalem7  27315  basellem9  27325  muinv  27429  dchrmullid  27488  dchrinvcl  27489  dchrisum0lem2a  27753  logdivsum  27769  mulog2sumlem1  27770  log2sumbnd  27780  hilnormi  31644  chscllem4  32121  hmopidmchi  32632  rabfodom  32980  ofoprabco  33137  fpwrelmapffslem  33203  fpwrelmap  33204  prodindf  33308  gsummulsubdishift1  33508  gsumwrd2dccat  33518  elrgspn  33686  elrgspnsubrunlem2  33688  domnprodeq0  33719  deg1prod  33993  selvply1rhmlem2  34031  selvply1rhmlem4  34033  selvply1rhm0  34036  mplmulmvr  34049  evlextv  34052  mplvrpmfgalem  34054  mplvrpmga  34055  mplvrpmrhm  34057  psrgsum  34058  psrmonmul  34060  psrmonprod  34062  issply  34071  esplyfval0  34074  esplyfvaln  34084  lbsdiflsp0  34136  fedgmullem1  34139  extdgfialglem2  34203  qqhre  34530  esumpcvgval  34588  ofcfval4  34615  omssubadd  34811  carsggect  34829  fdvneggt  35108  fdvnegge  35110  itgexpif  35114  ptpconn  35812  cvmliftlem6  35869  cvmliftlem8  35871  cvmlift2lem7  35888  cvmliftphtlem  35896  cvmlift3lem5  35902  elmsubrn  36107  knoppcnlem9  37198  curunc  38356  poimir  38402  broucube  38403  mblfinlem2  38407  volsupnfl  38414  cnambfre  38417  dvtan  38419  itg2addnclem  38420  itg2addnclem2  38421  itg2addnclem3  38422  itg2addnc  38423  itg2gt0cn  38424  itgaddnc  38429  itgmulc2nc  38437  ftc1cnnclem  38440  ftc1anclem1  38442  ftc1anclem2  38443  ftc1anclem3  38444  ftc1anclem4  38445  ftc1anclem5  38446  ftc1anclem6  38447  ftc1anclem7  38448  ftc1anclem8  38449  ftc1anc  38450  ftc2nc  38451  upixp  38479  readvcot  43239  evlselv  43435  fsuppssindlem1  43437  fsuppssindlem2  43438  mhphflem  43442  mhphf  43443  mzpsubst  43593  diophun  43618  mendlmod  44030  mendassa  44031  cantnf2  44166  fsovcnvlem  44853  binomcxplemnotnn0  45180  rnsnf  46016  cncfmptss  46417  climliminflimsupd  46629  mulcncff  46698  subcncff  46708  cncfcompt  46711  addcncff  46712  divcncff  46719  cncfiooicclem1  46721  dvsinexp  46739  dvsubf  46742  dvdivf  46750  dvcosax  46754  dvnmul  46771  dvnprodlem1  46774  dvnprodlem2  46775  itgsinexplem1  46782  itgsubsticclem  46803  iblcncfioo  46806  itgiccshift  46808  stoweidlem20  46848  dirkercncflem2  46932  fourierdlem16  46951  fourierdlem21  46956  fourierdlem22  46957  fourierdlem28  46963  fourierdlem39  46974  fourierdlem51  46985  fourierdlem60  46994  fourierdlem61  46995  fourierdlem69  47003  fourierdlem72  47006  fourierdlem73  47007  fourierdlem81  47015  fourierdlem83  47017  fourierdlem84  47018  fourierdlem87  47021  fourierdlem90  47024  fourierdlem93  47027  fourierdlem95  47029  fourierdlem101  47035  fourierdlem103  47037  fourierdlem104  47038  fourierdlem111  47045  etransclem34  47096  etransclem43  47105  etransclem46  47108  sge0tsms  47208  sge0fodjrnlem  47244  sge0iun  47247  sge0isum  47255  sge0seq  47274  meadjun  47290  meadjiunlem  47293  meadjiun  47294  ismeannd  47295  psmeasurelem  47298  omeiunle  47345  ovn02  47396  smfpimioo  47615  smfresal  47616  smfinflem  47645  smflimsuplem3  47650  smfliminflem  47658  1arymaptfo  49573  diag1  50230  dvsec  50689  dvcsc  50690  dvcot  50691  aacllem  50772  amgmwlem  50820  amgmlemALT  50821