Theorem feqmptd 6947

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

Syntax hints:   → wi 4   = wceq 1567   ↦ cmpt 5193   Fn wfn 6529  ⟶wf 6530  ‘cfv 6534

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-sep 5258  ax-nul 5268  ax-pr 5402

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ne 2965  df-ral 3086  df-rex 3096  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4874  df-br 5111  df-opab 5175  df-mpt 5194  df-id 5554  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-iota 6490  df-fun 6536  df-fn 6537  df-f 6538  df-fv 6542

This theorem is referenced by:  feqresmpt  6948  cofmpt  7126  fcoconst  7128  ofco  7697  caofinvl  7704  caofcom  7709  caofidlcan  7710  caofass  7712  caofdi  7714  caofdir  7715  caonncan  7716  suppssof1  8191  mapxpen  9127  xpmapenlem  9128  cantnfp1  9646  cantnflem1  9654  cnfcom2lem  9666  infxpenc  9998  pwfseqlem5  10644  gruf  10792  ccatco  14868  cnrecnv  15212  rlimclim1  15592  rlimuni  15597  lo1resb  15611  rlimresb  15612  o1resb  15613  rlimcn1  15635  rlimo1  15664  o1rlimmul  15666  caucvgr  15723  ackbijnn  15878  bitsf1ocnv  16498  ramcl  17085  pwsplusgval  17540  pwsmulrval  17541  pwsvscafval  17544  setcepi  18141  prf1st  18256  prf2nd  18257  1st2ndprf  18258  curfuncf  18290  curf2ndf  18299  yonedainv  18333  yonffthlem  18334  prdsidlem  18823  mhmvlin  18855  pwsco1mhm  18887  pwsco2mhm  18888  frmdup3lem  18921  frmdup3  18922  grpinvcnv  19069  pwsinvg  19115  pwssub  19116  efginvrel1  19794  frgpup3lem  19843  frgpup3  19844  gsumval3  19973  gsumcllem  19974  gsumzf1o  19978  gsumzsplit  19993  gsumconst  20000  gsumzmhm  20003  gsumsub  20014  gsum2dlem2  20037  gsumcom2  20041  dprdfadd  20088  dprdfsub  20089  dprdfeq0  20090  dprdf11  20091  dmdprdsplitlem  20105  dprddisj2  20107  dpjidcl  20126  ablfaclem2  20154  ablfac2  20157  rrgsupp  20782  mptscmfsuppd  21023  lmhmvsca  21140  mulgrhm2  21593  cygznlem2a  21682  frgpcyg  21688  uvcresum  21908  frlmup1  21913  gsumbagdiaglem  22046  psrass1lem  22048  psrlinv  22070  psrass1  22078  psrcom  22082  mplsubrglem  22118  mplmonmul  22152  mplcoe1  22153  mplcoe5  22156  evlslem2  22195  evlslem6  22197  evlslem1  22198  selvvvval  22258  mhpmulcl  22277  psdmplcl  22290  psdmul  22294  coe1fval3  22333  coe1sclmul  22408  coe1sclmul2  22410  grpvrinv  22521  mdetleib2  22710  mdetunilem9  22742  cayleyhamilton1  23014  neiptopnei  23254  dfac14  23740  ptcnp  23744  lmcn2  23771  cnmpt11f  23786  cnmpt21f  23794  cnmpt2k  23810  qtopeu  23838  xkocnv  23936  xkohmeo  23937  flfcnp2  24129  istgp2  24213  tmdgsum  24217  subgtgp  24227  symgtgp  24228  tgpconncomp  24235  prdstgpd  24247  tsmssub  24271  tgptsmscls  24272  tsmssplit  24274  tsmsxplem1  24275  tlmtgp  24318  ustuqtop  24368  prdsmslem1  24649  prdsxmslem1  24650  prdsxmslem2  24651  tngnm  24773  nmoeq0  24858  cnfldnm  24900  cncfmpt1f  25038  negfcncf  25047  cnrehmeo  25077  evth  25083  evth2  25084  copco  25142  pcopt  25146  pcopt2  25147  pcoass  25148  pcorev2  25152  pi1xfrcnv  25181  ovolctb  25614  ovolfs2  25695  uniioombllem2  25707  ismbf  25752  mbfconst  25757  mbfmulc2re  25772  mbfadd  25785  mbfsub  25786  mbflimsup  25790  mbfi1flimlem  25846  mbfi1flim  25847  mbfmul  25850  itg2uba  25867  itg2mulclem  25870  itg2mulc  25871  itg2splitlem  25872  itg2monolem1  25874  itg2i1fseq  25879  itg2gt0  25884  itg2cnlem1  25885  itg2cnlem2  25886  i1fibl  25932  itgitg1  25933  bddmulibl  25963  bddiblnc  25966  cnplimc  26011  limccnp2  26016  dvcnp2  26044  dvmulf  26067  dvcmulf  26069  dvcobr  26070  dvcof  26072  dvcj  26074  dvfre  26075  dvmptcj  26092  dvcnvlem  26100  dvcnv  26101  dvef  26104  dvsincos  26105  rolle  26114  cmvth  26115  dvlip  26117  dvlipcn  26118  dv11cn  26125  dvivthlem1  26132  dvivth  26134  lhop2  26139  dvfsumrlim2  26156  ftc1lem1  26159  ftc1lem2  26160  ftc1a  26161  ftc1lem4  26163  ftc2  26168  ftc2ditglem  26169  ftc2ditg  26170  tdeglem4  26182  tdeglem2  26183  mdegle0  26199  mdegmullem  26200  plypf1  26334  plyco  26363  dgrcolem1  26395  dgrcolem2  26396  dgrco  26397  plycjlem  26398  plyn0mulidp  26407  dvply2g  26411  plydiveu  26424  elqaalem3  26447  taylthlem1  26498  taylthlem2  26499  ulmshft  26515  ulmdvlem1  26525  mtest  26529  mtestbdd  26530  mbfulm  26531  iblulm  26532  itgulm  26533  pserulm  26547  pserdv  26554  abelthlem1  26556  abelthlem3  26558  pige3ALT  26647  eff1olem  26675  logcn  26774  advlog  26781  advlogexp  26782  logtayl  26787  logccv  26790  dvcxp1  26867  dvcxp2  26868  dvcncxp1  26870  resqrtcn  26876  sqrtcn  26877  loglesqrt  26888  dvatan  27062  leibpi  27069  divsqrtsumo1  27110  jensenlem2  27114  amgmlem  27116  lgamgulmlem2  27156  ftalem7  27205  basellem9  27215  muinv  27319  dchrmullid  27378  dchrinvcl  27379  dchrisum0lem2a  27643  logdivsum  27659  mulog2sumlem1  27660  log2sumbnd  27670  hilnormi  31452  chscllem4  31929  hmopidmchi  32440  rabfodom  32788  ofoprabco  32946  fpwrelmapffslem  33014  fpwrelmap  33015  prodindf  33119  gsummulsubdishift1  33325  gsumwrd2dccat  33335  elrgspn  33503  elrgspnsubrunlem2  33505  domnprodeq0  33536  deg1prod  33814  selvply1rhmlem2  33852  selvply1rhmlem4  33854  selvply1rhm0  33857  mplmulmvr  33870  evlextv  33873  mplvrpmfgalem  33875  mplvrpmga  33876  mplvrpmrhm  33878  psrgsum  33879  psrmonmul  33881  psrmonprod  33883  issply  33892  esplyfval0  33895  esplyfvaln  33905  lbsdiflsp0  33957  fedgmullem1  33960  extdgfialglem2  34024  qqhre  34351  esumpcvgval  34409  ofcfval4  34436  omssubadd  34631  carsggect  34649  fdvneggt  34928  fdvnegge  34930  itgexpif  34934  ptpconn  35620  cvmliftlem6  35677  cvmliftlem8  35679  cvmlift2lem7  35696  cvmliftphtlem  35704  cvmlift3lem5  35710  elmsubrn  35915  knoppcnlem9  36975  curunc  38136  poimir  38187  broucube  38188  mblfinlem2  38192  volsupnfl  38199  cnambfre  38202  dvtan  38204  itg2addnclem  38205  itg2addnclem2  38206  itg2addnclem3  38207  itg2addnc  38208  itg2gt0cn  38209  itgaddnc  38214  itgmulc2nc  38222  ftc1cnnclem  38225  ftc1anclem1  38227  ftc1anclem2  38228  ftc1anclem3  38229  ftc1anclem4  38230  ftc1anclem5  38231  ftc1anclem6  38232  ftc1anclem7  38233  ftc1anclem8  38234  ftc1anc  38235  ftc2nc  38236  upixp  38263  readvcot  43010  evlselv  43208  fsuppssindlem1  43210  fsuppssindlem2  43211  mhphflem  43215  mhphf  43216  mzpsubst  43366  diophun  43391  mendlmod  43803  mendassa  43804  cantnf2  43939  fsovcnvlem  44626  binomcxplemnotnn0  44953  rnsnf  45789  cncfmptss  46190  climliminflimsupd  46402  mulcncff  46471  subcncff  46481  cncfcompt  46484  addcncff  46485  divcncff  46492  cncfiooicclem1  46494  dvsinexp  46512  dvsubf  46515  dvdivf  46523  dvcosax  46527  dvnmul  46544  dvnprodlem1  46547  dvnprodlem2  46548  itgsinexplem1  46555  itgsubsticclem  46576  iblcncfioo  46579  itgiccshift  46581  stoweidlem20  46621  dirkercncflem2  46705  fourierdlem16  46724  fourierdlem21  46729  fourierdlem22  46730  fourierdlem28  46736  fourierdlem39  46747  fourierdlem51  46758  fourierdlem60  46767  fourierdlem61  46768  fourierdlem69  46776  fourierdlem72  46779  fourierdlem73  46780  fourierdlem81  46788  fourierdlem83  46790  fourierdlem84  46791  fourierdlem87  46794  fourierdlem90  46797  fourierdlem93  46800  fourierdlem95  46802  fourierdlem101  46808  fourierdlem103  46810  fourierdlem104  46811  fourierdlem111  46818  etransclem34  46869  etransclem43  46878  etransclem46  46881  sge0tsms  46981  sge0fodjrnlem  47017  sge0iun  47020  sge0isum  47028  sge0seq  47047  meadjun  47063  meadjiunlem  47066  meadjiun  47067  ismeannd  47068  psmeasurelem  47071  omeiunle  47118  ovn02  47169  smfpimioo  47388  smfresal  47389  smfinflem  47418  smflimsuplem3  47423  smfliminflem  47431  1arymaptfo  49303  diag1  49962  aacllem  50470  amgmwlem  50471  amgmlemALT  50472