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 6706	. 2 ⊢ (𝜑 → 𝐹 Fn 𝐴)
3		dffn5 6936	. 2 ⊢ (𝐹 Fn 𝐴 ↔ 𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)))
4	2, 3	sylib 218	1 ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)))

Syntax hints:   → wi 4   = wceq 1540   ↦ cmpt 5201   Fn wfn 6525  ⟶wf 6526  ‘cfv 6530

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 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pr 5402

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 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2809  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3061  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-opab 5182  df-mpt 5202  df-id 5548  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-iota 6483  df-fun 6532  df-fn 6533  df-f 6534  df-fv 6538

This theorem is referenced by:  feqresmpt  6947  cofmpt  7121  fcoconst  7123  ofco  7694  caofinvl  7701  caofcom  7706  caofidlcan  7707  caofass  7709  caofdi  7711  caofdir  7712  caonncan  7713  suppssof1  8196  mapxpen  9155  xpmapenlem  9156  cantnfp1  9693  cantnflem1  9701  cnfcom2lem  9713  infxpenc  10030  pwfseqlem5  10675  gruf  10823  ccatco  14852  cnrecnv  15182  rlimclim1  15559  rlimuni  15564  lo1resb  15578  rlimresb  15579  o1resb  15580  rlimcn1  15602  rlimo1  15631  o1rlimmul  15633  caucvgr  15690  ackbijnn  15842  bitsf1ocnv  16461  ramcl  17047  pwsplusgval  17502  pwsmulrval  17503  pwsvscafval  17506  setcepi  18099  prf1st  18214  prf2nd  18215  1st2ndprf  18216  curfuncf  18248  curf2ndf  18257  yonedainv  18291  yonffthlem  18292  prdsidlem  18745  mhmvlin  18777  pwsco1mhm  18808  pwsco2mhm  18809  frmdup3lem  18842  frmdup3  18843  grpinvcnv  18987  pwsinvg  19034  pwssub  19035  efginvrel1  19707  frgpup3lem  19756  frgpup3  19757  gsumval3  19886  gsumcllem  19887  gsumzf1o  19891  gsumzsplit  19906  gsumconst  19913  gsumzmhm  19916  gsumsub  19927  gsum2dlem2  19950  gsumcom2  19954  dprdfadd  20001  dprdfsub  20002  dprdfeq0  20003  dprdf11  20004  dmdprdsplitlem  20018  dprddisj2  20020  dpjidcl  20039  ablfaclem2  20067  ablfac2  20070  rrgsupp  20659  mptscmfsuppd  20883  lmhmvsca  21001  mulgrhm2  21437  cygznlem2a  21526  frgpcyg  21532  uvcresum  21751  frlmup1  21756  gsumbagdiaglem  21888  psrass1lem  21890  psrlinv  21913  psrass1  21922  psrcom  21926  mplsubrglem  21962  mplmonmul  21992  mplcoe1  21993  mplcoe5  21996  evlslem2  22035  evlslem6  22037  evlslem1  22038  mhpmulcl  22085  psdmplcl  22098  psdmul  22102  coe1fval3  22142  coe1sclmul  22217  coe1sclmul2  22219  grpvrinv  22335  mdetleib2  22524  mdetunilem9  22556  cayleyhamilton1  22828  neiptopnei  23068  dfac14  23554  ptcnp  23558  lmcn2  23585  cnmpt11f  23600  cnmpt21f  23608  cnmpt2k  23624  qtopeu  23652  xkocnv  23750  xkohmeo  23751  flfcnp2  23943  istgp2  24027  tmdgsum  24031  subgtgp  24041  symgtgp  24042  tgpconncomp  24049  prdstgpd  24061  tsmssub  24085  tgptsmscls  24086  tsmssplit  24088  tsmsxplem1  24089  tlmtgp  24132  ustuqtop  24183  prdsmslem1  24464  prdsxmslem1  24465  prdsxmslem2  24466  tngnm  24588  nmoeq0  24673  cnfldnm  24715  cncfmpt1f  24856  negfcncf  24866  cnrehmeo  24900  cnrehmeoOLD  24901  evth  24907  evth2  24908  copco  24967  pcopt  24971  pcopt2  24972  pcoass  24973  pcorev2  24977  pi1xfrcnv  25006  ovolctb  25441  ovolfs2  25522  uniioombllem2  25534  ismbf  25579  mbfconst  25584  mbfmulc2re  25599  mbfadd  25612  mbfsub  25613  mbflimsup  25617  mbfi1flimlem  25673  mbfi1flim  25674  mbfmul  25677  itg2uba  25694  itg2mulclem  25697  itg2mulc  25698  itg2splitlem  25699  itg2monolem1  25701  itg2i1fseq  25706  itg2gt0  25711  itg2cnlem1  25712  itg2cnlem2  25713  i1fibl  25759  itgitg1  25760  bddmulibl  25790  bddiblnc  25793  cnplimc  25838  limccnp2  25843  dvcnp2  25871  dvcnp2OLD  25872  dvmulf  25896  dvcmulf  25898  dvcobr  25899  dvcobrOLD  25900  dvcof  25902  dvcj  25904  dvfre  25905  dvmptcj  25922  dvcnvlem  25930  dvcnv  25931  dvef  25934  dvsincos  25935  rolle  25944  cmvth  25945  cmvthOLD  25946  dvlip  25948  dvlipcn  25949  dv11cn  25956  dvivthlem1  25963  dvivth  25965  lhop2  25970  dvfsumrlim2  25989  ftc1lem1  25992  ftc1lem2  25993  ftc1a  25994  ftc1lem4  25996  ftc2  26001  ftc2ditglem  26002  ftc2ditg  26003  tdeglem4  26015  tdeglem2  26016  mdegle0  26032  mdegmullem  26033  plypf1  26167  plyco  26196  dgrcolem1  26229  dgrcolem2  26230  dgrco  26231  plycjlem  26232  dvply2g  26242  dvply2gOLD  26243  plydiveu  26256  elqaalem3  26279  taylthlem1  26331  taylthlem2  26332  taylthlem2OLD  26333  ulmshft  26349  ulmdvlem1  26359  mtest  26363  mtestbdd  26364  mbfulm  26365  iblulm  26366  itgulm  26367  pserulm  26381  pserdv  26389  abelthlem1  26391  abelthlem3  26393  pige3ALT  26479  eff1olem  26507  logcn  26606  advlog  26613  advlogexp  26614  logtayl  26619  logccv  26622  dvcxp1  26699  dvcxp2  26700  dvcncxp1  26702  resqrtcn  26709  sqrtcn  26710  loglesqrt  26721  dvatan  26895  leibpi  26902  divsqrtsumo1  26944  jensenlem2  26948  amgmlem  26950  lgamgulmlem2  26990  ftalem7  27039  basellem9  27049  muinv  27153  dchrmullid  27213  dchrinvcl  27214  dchrisum0lem2a  27478  logdivsum  27494  mulog2sumlem1  27495  log2sumbnd  27505  hilnormi  31090  chscllem4  31567  hmopidmchi  32078  rabfodom  32432  ofoprabco  32588  fpwrelmapffslem  32655  fpwrelmap  32656  prodindf  32786  gsumwrd2dccat  33007  elrgspn  33187  elrgspnsubrunlem2  33189  lbsdiflsp0  33612  fedgmullem1  33615  qqhre  33997  esumpcvgval  34055  ofcfval4  34082  omssubadd  34278  carsggect  34296  plymulx0  34525  fdvneggt  34578  fdvnegge  34580  itgexpif  34584  ptpconn  35201  cvmliftlem6  35258  cvmliftlem8  35260  cvmlift2lem7  35277  cvmliftphtlem  35285  cvmlift3lem5  35291  elmsubrn  35496  knoppcnlem9  36465  curunc  37572  poimir  37623  broucube  37624  mblfinlem2  37628  volsupnfl  37635  cnambfre  37638  dvtan  37640  itg2addnclem  37641  itg2addnclem2  37642  itg2addnclem3  37643  itg2addnc  37644  itg2gt0cn  37645  itgaddnc  37650  itgmulc2nc  37658  ftc1cnnclem  37661  ftc1anclem1  37663  ftc1anclem2  37664  ftc1anclem3  37665  ftc1anclem4  37666  ftc1anclem5  37667  ftc1anclem6  37668  ftc1anclem7  37669  ftc1anclem8  37670  ftc1anc  37671  ftc2nc  37672  upixp  37699  readvcot  42354  selvvvval  42555  evlselv  42557  fsuppssindlem1  42561  fsuppssindlem2  42562  mhphflem  42566  mhphf  42567  mzpsubst  42718  diophun  42743  mendlmod  43160  mendassa  43161  cantnf2  43296  fsovcnvlem  43984  binomcxplemnotnn0  44328  rnsnf  45156  cncfmptss  45564  climliminflimsupd  45778  mulcncff  45847  subcncff  45857  cncfcompt  45860  addcncff  45861  divcncff  45868  cncfiooicclem1  45870  dvsinexp  45888  dvsubf  45891  dvdivf  45899  dvcosax  45903  dvnmul  45920  dvnprodlem1  45923  dvnprodlem2  45924  itgsinexplem1  45931  itgsubsticclem  45952  iblcncfioo  45955  itgiccshift  45957  stoweidlem20  45997  dirkercncflem2  46081  fourierdlem16  46100  fourierdlem21  46105  fourierdlem22  46106  fourierdlem28  46112  fourierdlem39  46123  fourierdlem51  46134  fourierdlem60  46143  fourierdlem61  46144  fourierdlem69  46152  fourierdlem72  46155  fourierdlem73  46156  fourierdlem81  46164  fourierdlem83  46166  fourierdlem84  46167  fourierdlem87  46170  fourierdlem90  46173  fourierdlem93  46176  fourierdlem95  46178  fourierdlem101  46184  fourierdlem103  46186  fourierdlem104  46187  fourierdlem111  46194  etransclem34  46245  etransclem43  46254  etransclem46  46257  sge0tsms  46357  sge0fodjrnlem  46393  sge0iun  46396  sge0isum  46404  sge0seq  46423  meadjun  46439  meadjiunlem  46442  meadjiun  46443  ismeannd  46444  psmeasurelem  46447  omeiunle  46494  ovn02  46545  smfpimioo  46764  smfresal  46765  smfinflem  46794  smflimsuplem3  46799  smfliminflem  46807  1arymaptfo  48571  diag1  49163  aacllem  49613  amgmwlem  49614  amgmlemALT  49615