Theorem feqmptd 6990

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

Syntax hints:   → wi 4   = wceq 1537   ↦ cmpt 5249   Fn wfn 6568  ⟶wf 6569  ‘cfv 6573

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pr 5447

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ne 2947  df-ral 3068  df-rex 3077  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-opab 5229  df-mpt 5250  df-id 5593  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-iota 6525  df-fun 6575  df-fn 6576  df-f 6577  df-fv 6581

This theorem is referenced by:  feqresmpt  6991  cofmpt  7166  fcoconst  7168  ofco  7738  caofinvl  7745  caofcom  7750  caofass  7752  caofdi  7754  caofdir  7755  caonncan  7756  suppssof1  8240  mapxpen  9209  xpmapenlem  9210  cantnfp1  9750  cantnflem1  9758  cnfcom2lem  9770  infxpenc  10087  pwfseqlem5  10732  gruf  10880  ccatco  14884  cnrecnv  15214  rlimclim1  15591  rlimuni  15596  lo1resb  15610  rlimresb  15611  o1resb  15612  rlimcn1  15634  rlimo1  15663  o1rlimmul  15665  caucvgr  15724  ackbijnn  15876  bitsf1ocnv  16490  ramcl  17076  pwsplusgval  17550  pwsmulrval  17551  pwsvscafval  17554  setcepi  18155  prf1st  18273  prf2nd  18274  1st2ndprf  18275  curfuncf  18308  curf2ndf  18317  yonedainv  18351  yonffthlem  18352  prdsidlem  18804  mhmvlin  18836  pwsco1mhm  18867  pwsco2mhm  18868  frmdup3lem  18901  frmdup3  18902  grpinvcnv  19046  pwsinvg  19093  pwssub  19094  efginvrel1  19770  frgpup3lem  19819  frgpup3  19820  gsumval3  19949  gsumcllem  19950  gsumzf1o  19954  gsumzsplit  19969  gsumconst  19976  gsumzmhm  19979  gsumsub  19990  gsum2dlem2  20013  gsumcom2  20017  dprdfadd  20064  dprdfsub  20065  dprdfeq0  20066  dprdf11  20067  dmdprdsplitlem  20081  dprddisj2  20083  dpjidcl  20102  ablfaclem2  20130  ablfac2  20133  rrgsupp  20723  mptscmfsuppd  20948  lmhmvsca  21067  mulgrhm2  21512  cygznlem2a  21609  frgpcyg  21615  uvcresum  21836  frlmup1  21841  gsumbagdiaglem  21973  psrass1lem  21975  psrlinv  21998  psrass1  22007  psrcom  22011  mplsubrglem  22047  mplmonmul  22077  mplcoe1  22078  mplcoe5  22081  evlslem2  22126  evlslem6  22128  evlslem1  22129  mhpmulcl  22176  psdmplcl  22189  psdmul  22193  coe1fval3  22231  coe1sclmul  22306  coe1sclmul2  22308  grpvrinv  22424  mdetleib2  22615  mdetunilem9  22647  cayleyhamilton1  22919  neiptopnei  23161  dfac14  23647  ptcnp  23651  lmcn2  23678  cnmpt11f  23693  cnmpt21f  23701  cnmpt2k  23717  qtopeu  23745  xkocnv  23843  xkohmeo  23844  flfcnp2  24036  istgp2  24120  tmdgsum  24124  subgtgp  24134  symgtgp  24135  tgpconncomp  24142  prdstgpd  24154  tsmssub  24178  tgptsmscls  24179  tsmssplit  24181  tsmsxplem1  24182  tlmtgp  24225  ustuqtop  24276  prdsmslem1  24561  prdsxmslem1  24562  prdsxmslem2  24563  tngnm  24693  nmoeq0  24778  cnfldnm  24820  cncfmpt1f  24959  negfcncf  24969  cnrehmeo  25003  cnrehmeoOLD  25004  evth  25010  evth2  25011  copco  25070  pcopt  25074  pcopt2  25075  pcoass  25076  pcorev2  25080  pi1xfrcnv  25109  ovolctb  25544  ovolfs2  25625  uniioombllem2  25637  ismbf  25682  mbfconst  25687  mbfmulc2re  25702  mbfadd  25715  mbfsub  25716  mbflimsup  25720  mbfi1flimlem  25777  mbfi1flim  25778  mbfmul  25781  itg2uba  25798  itg2mulclem  25801  itg2mulc  25802  itg2splitlem  25803  itg2monolem1  25805  itg2i1fseq  25810  itg2gt0  25815  itg2cnlem1  25816  itg2cnlem2  25817  i1fibl  25863  itgitg1  25864  bddmulibl  25894  bddiblnc  25897  cnplimc  25942  limccnp2  25947  dvcnp2  25975  dvcnp2OLD  25976  dvmulf  26000  dvcmulf  26002  dvcobr  26003  dvcobrOLD  26004  dvcof  26006  dvcj  26008  dvfre  26009  dvmptcj  26026  dvcnvlem  26034  dvcnv  26035  dvef  26038  dvsincos  26039  rolle  26048  cmvth  26049  cmvthOLD  26050  dvlip  26052  dvlipcn  26053  dv11cn  26060  dvivthlem1  26067  dvivth  26069  lhop2  26074  dvfsumrlim2  26093  ftc1lem1  26096  ftc1lem2  26097  ftc1a  26098  ftc1lem4  26100  ftc2  26105  ftc2ditglem  26106  ftc2ditg  26107  tdeglem4  26119  tdeglem2  26120  mdegle0  26136  mdegmullem  26137  plypf1  26271  plyco  26300  dgrcolem1  26333  dgrcolem2  26334  dgrco  26335  plycjlem  26336  dvply2g  26344  dvply2gOLD  26345  plydiveu  26358  elqaalem3  26381  taylthlem1  26433  taylthlem2  26434  taylthlem2OLD  26435  ulmshft  26451  ulmdvlem1  26461  mtest  26465  mtestbdd  26466  mbfulm  26467  iblulm  26468  itgulm  26469  pserulm  26483  pserdv  26491  abelthlem1  26493  abelthlem3  26495  pige3ALT  26580  eff1olem  26608  logcn  26707  advlog  26714  advlogexp  26715  logtayl  26720  logccv  26723  dvcxp1  26800  dvcxp2  26801  dvcncxp1  26803  resqrtcn  26810  sqrtcn  26811  loglesqrt  26822  dvatan  26996  leibpi  27003  divsqrtsumo1  27045  jensenlem2  27049  amgmlem  27051  lgamgulmlem2  27091  ftalem7  27140  basellem9  27150  muinv  27254  dchrmullid  27314  dchrinvcl  27315  dchrisum0lem2a  27579  logdivsum  27595  mulog2sumlem1  27596  log2sumbnd  27606  hilnormi  31195  chscllem4  31672  hmopidmchi  32183  rabfodom  32533  ofoprabco  32682  fpwrelmapffslem  32746  fpwrelmap  32747  lbsdiflsp0  33639  fedgmullem1  33642  qqhre  33966  prodindf  33987  esumpcvgval  34042  ofcfval4  34069  omssubadd  34265  carsggect  34283  plymulx0  34524  fdvneggt  34577  fdvnegge  34579  itgexpif  34583  ptpconn  35201  cvmliftlem6  35258  cvmliftlem8  35260  cvmlift2lem7  35277  cvmliftphtlem  35285  cvmlift3lem5  35291  elmsubrn  35496  knoppcnlem9  36467  curunc  37562  poimir  37613  broucube  37614  mblfinlem2  37618  volsupnfl  37625  cnambfre  37628  dvtan  37630  itg2addnclem  37631  itg2addnclem2  37632  itg2addnclem3  37633  itg2addnc  37634  itg2gt0cn  37635  itgaddnc  37640  itgmulc2nc  37648  ftc1cnnclem  37651  ftc1anclem1  37653  ftc1anclem2  37654  ftc1anclem3  37655  ftc1anclem4  37656  ftc1anclem5  37657  ftc1anclem6  37658  ftc1anclem7  37659  ftc1anclem8  37660  ftc1anc  37661  ftc2nc  37662  upixp  37689  selvvvval  42540  evlselv  42542  fsuppssindlem1  42546  fsuppssindlem2  42547  mhphflem  42551  mhphf  42552  mzpsubst  42704  diophun  42729  mendlmod  43150  mendassa  43151  cantnf2  43287  fsovcnvlem  43975  binomcxplemnotnn0  44325  rnsnf  45091  cncfmptss  45508  climliminflimsupd  45722  mulcncff  45791  subcncff  45801  cncfcompt  45804  addcncff  45805  divcncff  45812  cncfiooicclem1  45814  dvsinexp  45832  dvsubf  45835  dvdivf  45843  dvcosax  45847  dvnmul  45864  dvnprodlem1  45867  dvnprodlem2  45868  itgsinexplem1  45875  itgsubsticclem  45896  iblcncfioo  45899  itgiccshift  45901  stoweidlem20  45941  dirkercncflem2  46025  fourierdlem16  46044  fourierdlem21  46049  fourierdlem22  46050  fourierdlem28  46056  fourierdlem39  46067  fourierdlem51  46078  fourierdlem60  46087  fourierdlem61  46088  fourierdlem69  46096  fourierdlem72  46099  fourierdlem73  46100  fourierdlem81  46108  fourierdlem83  46110  fourierdlem84  46111  fourierdlem87  46114  fourierdlem90  46117  fourierdlem93  46120  fourierdlem95  46122  fourierdlem101  46128  fourierdlem103  46130  fourierdlem104  46131  fourierdlem111  46138  etransclem34  46189  etransclem43  46198  etransclem46  46201  sge0tsms  46301  sge0fodjrnlem  46337  sge0iun  46340  sge0isum  46348  sge0seq  46367  meadjun  46383  meadjiunlem  46386  meadjiun  46387  ismeannd  46388  psmeasurelem  46391  omeiunle  46438  ovn02  46489  smfpimioo  46708  smfresal  46709  smfinflem  46738  smflimsuplem3  46743  smfliminflem  46751  1arymaptfo  48377  aacllem  48895  amgmwlem  48896  amgmlemALT  48897