Theorem feqmptd 6895

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

Syntax hints:   → wi 4   = wceq 1540   ↦ cmpt 5176   Fn wfn 6481  ⟶wf 6482  ‘cfv 6486

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5238  ax-nul 5248  ax-pr 5374

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-rab 3397  df-v 3440  df-dif 3908  df-un 3910  df-ss 3922  df-nul 4287  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4862  df-br 5096  df-opab 5158  df-mpt 5177  df-id 5518  df-xp 5629  df-rel 5630  df-cnv 5631  df-co 5632  df-dm 5633  df-iota 6442  df-fun 6488  df-fn 6489  df-f 6490  df-fv 6494

This theorem is referenced by:  feqresmpt  6896  cofmpt  7070  fcoconst  7072  ofco  7642  caofinvl  7649  caofcom  7654  caofidlcan  7655  caofass  7657  caofdi  7659  caofdir  7660  caonncan  7661  suppssof1  8139  mapxpen  9067  xpmapenlem  9068  cantnfp1  9596  cantnflem1  9604  cnfcom2lem  9616  infxpenc  9931  pwfseqlem5  10576  gruf  10724  ccatco  14761  cnrecnv  15091  rlimclim1  15471  rlimuni  15476  lo1resb  15490  rlimresb  15491  o1resb  15492  rlimcn1  15514  rlimo1  15543  o1rlimmul  15545  caucvgr  15602  ackbijnn  15754  bitsf1ocnv  16374  ramcl  16960  pwsplusgval  17413  pwsmulrval  17414  pwsvscafval  17417  setcepi  18014  prf1st  18129  prf2nd  18130  1st2ndprf  18131  curfuncf  18163  curf2ndf  18172  yonedainv  18206  yonffthlem  18207  prdsidlem  18662  mhmvlin  18694  pwsco1mhm  18725  pwsco2mhm  18726  frmdup3lem  18759  frmdup3  18760  grpinvcnv  18904  pwsinvg  18951  pwssub  18952  efginvrel1  19626  frgpup3lem  19675  frgpup3  19676  gsumval3  19805  gsumcllem  19806  gsumzf1o  19810  gsumzsplit  19825  gsumconst  19832  gsumzmhm  19835  gsumsub  19846  gsum2dlem2  19869  gsumcom2  19873  dprdfadd  19920  dprdfsub  19921  dprdfeq0  19922  dprdf11  19923  dmdprdsplitlem  19937  dprddisj2  19939  dpjidcl  19958  ablfaclem2  19986  ablfac2  19989  rrgsupp  20605  mptscmfsuppd  20850  lmhmvsca  20968  mulgrhm2  21404  cygznlem2a  21493  frgpcyg  21499  uvcresum  21719  frlmup1  21724  gsumbagdiaglem  21856  psrass1lem  21858  psrlinv  21881  psrass1  21890  psrcom  21894  mplsubrglem  21930  mplmonmul  21960  mplcoe1  21961  mplcoe5  21964  evlslem2  22003  evlslem6  22005  evlslem1  22006  mhpmulcl  22053  psdmplcl  22066  psdmul  22070  coe1fval3  22110  coe1sclmul  22185  coe1sclmul2  22187  grpvrinv  22303  mdetleib2  22492  mdetunilem9  22524  cayleyhamilton1  22796  neiptopnei  23036  dfac14  23522  ptcnp  23526  lmcn2  23553  cnmpt11f  23568  cnmpt21f  23576  cnmpt2k  23592  qtopeu  23620  xkocnv  23718  xkohmeo  23719  flfcnp2  23911  istgp2  23995  tmdgsum  23999  subgtgp  24009  symgtgp  24010  tgpconncomp  24017  prdstgpd  24029  tsmssub  24053  tgptsmscls  24054  tsmssplit  24056  tsmsxplem1  24057  tlmtgp  24100  ustuqtop  24151  prdsmslem1  24432  prdsxmslem1  24433  prdsxmslem2  24434  tngnm  24556  nmoeq0  24641  cnfldnm  24683  cncfmpt1f  24824  negfcncf  24834  cnrehmeo  24868  cnrehmeoOLD  24869  evth  24875  evth2  24876  copco  24935  pcopt  24939  pcopt2  24940  pcoass  24941  pcorev2  24945  pi1xfrcnv  24974  ovolctb  25408  ovolfs2  25489  uniioombllem2  25501  ismbf  25546  mbfconst  25551  mbfmulc2re  25566  mbfadd  25579  mbfsub  25580  mbflimsup  25584  mbfi1flimlem  25640  mbfi1flim  25641  mbfmul  25644  itg2uba  25661  itg2mulclem  25664  itg2mulc  25665  itg2splitlem  25666  itg2monolem1  25668  itg2i1fseq  25673  itg2gt0  25678  itg2cnlem1  25679  itg2cnlem2  25680  i1fibl  25726  itgitg1  25727  bddmulibl  25757  bddiblnc  25760  cnplimc  25805  limccnp2  25810  dvcnp2  25838  dvcnp2OLD  25839  dvmulf  25863  dvcmulf  25865  dvcobr  25866  dvcobrOLD  25867  dvcof  25869  dvcj  25871  dvfre  25872  dvmptcj  25889  dvcnvlem  25897  dvcnv  25898  dvef  25901  dvsincos  25902  rolle  25911  cmvth  25912  cmvthOLD  25913  dvlip  25915  dvlipcn  25916  dv11cn  25923  dvivthlem1  25930  dvivth  25932  lhop2  25937  dvfsumrlim2  25956  ftc1lem1  25959  ftc1lem2  25960  ftc1a  25961  ftc1lem4  25963  ftc2  25968  ftc2ditglem  25969  ftc2ditg  25970  tdeglem4  25982  tdeglem2  25983  mdegle0  25999  mdegmullem  26000  plypf1  26134  plyco  26163  dgrcolem1  26196  dgrcolem2  26197  dgrco  26198  plycjlem  26199  dvply2g  26209  dvply2gOLD  26210  plydiveu  26223  elqaalem3  26246  taylthlem1  26298  taylthlem2  26299  taylthlem2OLD  26300  ulmshft  26316  ulmdvlem1  26326  mtest  26330  mtestbdd  26331  mbfulm  26332  iblulm  26333  itgulm  26334  pserulm  26348  pserdv  26356  abelthlem1  26358  abelthlem3  26360  pige3ALT  26446  eff1olem  26474  logcn  26573  advlog  26580  advlogexp  26581  logtayl  26586  logccv  26589  dvcxp1  26666  dvcxp2  26667  dvcncxp1  26669  resqrtcn  26676  sqrtcn  26677  loglesqrt  26688  dvatan  26862  leibpi  26869  divsqrtsumo1  26911  jensenlem2  26915  amgmlem  26917  lgamgulmlem2  26957  ftalem7  27006  basellem9  27016  muinv  27120  dchrmullid  27180  dchrinvcl  27181  dchrisum0lem2a  27445  logdivsum  27461  mulog2sumlem1  27462  log2sumbnd  27472  hilnormi  31126  chscllem4  31603  hmopidmchi  32114  rabfodom  32468  ofoprabco  32626  fpwrelmapffslem  32694  fpwrelmap  32695  prodindf  32825  gsumwrd2dccat  33039  elrgspn  33205  elrgspnsubrunlem2  33207  mplvrpmfgalem  33564  mplvrpmga  33565  lbsdiflsp0  33612  fedgmullem1  33615  extdgfialglem2  33679  qqhre  34006  esumpcvgval  34064  ofcfval4  34091  omssubadd  34287  carsggect  34305  plymulx0  34534  fdvneggt  34587  fdvnegge  34589  itgexpif  34593  ptpconn  35225  cvmliftlem6  35282  cvmliftlem8  35284  cvmlift2lem7  35301  cvmliftphtlem  35309  cvmlift3lem5  35315  elmsubrn  35520  knoppcnlem9  36494  curunc  37601  poimir  37652  broucube  37653  mblfinlem2  37657  volsupnfl  37664  cnambfre  37667  dvtan  37669  itg2addnclem  37670  itg2addnclem2  37671  itg2addnclem3  37672  itg2addnc  37673  itg2gt0cn  37674  itgaddnc  37679  itgmulc2nc  37687  ftc1cnnclem  37690  ftc1anclem1  37692  ftc1anclem2  37693  ftc1anclem3  37694  ftc1anclem4  37695  ftc1anclem5  37696  ftc1anclem6  37697  ftc1anclem7  37698  ftc1anclem8  37699  ftc1anc  37700  ftc2nc  37701  upixp  37728  readvcot  42357  selvvvval  42578  evlselv  42580  fsuppssindlem1  42584  fsuppssindlem2  42585  mhphflem  42589  mhphf  42590  mzpsubst  42741  diophun  42766  mendlmod  43182  mendassa  43183  cantnf2  43318  fsovcnvlem  44006  binomcxplemnotnn0  44349  rnsnf  45182  cncfmptss  45588  climliminflimsupd  45802  mulcncff  45871  subcncff  45881  cncfcompt  45884  addcncff  45885  divcncff  45892  cncfiooicclem1  45894  dvsinexp  45912  dvsubf  45915  dvdivf  45923  dvcosax  45927  dvnmul  45944  dvnprodlem1  45947  dvnprodlem2  45948  itgsinexplem1  45955  itgsubsticclem  45976  iblcncfioo  45979  itgiccshift  45981  stoweidlem20  46021  dirkercncflem2  46105  fourierdlem16  46124  fourierdlem21  46129  fourierdlem22  46130  fourierdlem28  46136  fourierdlem39  46147  fourierdlem51  46158  fourierdlem60  46167  fourierdlem61  46168  fourierdlem69  46176  fourierdlem72  46179  fourierdlem73  46180  fourierdlem81  46188  fourierdlem83  46190  fourierdlem84  46191  fourierdlem87  46194  fourierdlem90  46197  fourierdlem93  46200  fourierdlem95  46202  fourierdlem101  46208  fourierdlem103  46210  fourierdlem104  46211  fourierdlem111  46218  etransclem34  46269  etransclem43  46278  etransclem46  46281  sge0tsms  46381  sge0fodjrnlem  46417  sge0iun  46420  sge0isum  46428  sge0seq  46447  meadjun  46463  meadjiunlem  46466  meadjiun  46467  ismeannd  46468  psmeasurelem  46471  omeiunle  46518  ovn02  46569  smfpimioo  46788  smfresal  46789  smfinflem  46818  smflimsuplem3  46823  smfliminflem  46831  1arymaptfo  48648  diag1  49309  aacllem  49806  amgmwlem  49807  amgmlemALT  49808