Theorem feqmptd 6949

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

Syntax hints:   → wi 4   = wceq 1570   ↦ cmpt 5192   Fn wfn 6531  ⟶wf 6532  ‘cfv 6536

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5257  ax-nul 5269  ax-pr 5404

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4488  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-br 5110  df-opab 5174  df-mpt 5193  df-id 5556  df-xp 5667  df-rel 5668  df-cnv 5669  df-co 5670  df-dm 5671  df-iota 6492  df-fun 6538  df-fn 6539  df-f 6540  df-fv 6544

This theorem is referenced by:  feqresmpt  6950  cofmpt  7128  fcoconst  7130  ofco  7699  caofinvl  7706  caofcom  7711  caofidlcan  7712  caofass  7714  caofdi  7716  caofdir  7717  caonncan  7718  suppssof1  8191  mapxpen  9127  xpmapenlem  9128  cantnfp1  9646  cantnflem1  9654  cnfcom2lem  9666  infxpenc  9998  pwfseqlem5  10643  gruf  10791  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  16497  ramcl  17084  pwsplusgval  17539  pwsmulrval  17540  pwsvscafval  17543  setcepi  18140  prf1st  18255  prf2nd  18256  1st2ndprf  18257  curfuncf  18289  curf2ndf  18298  yonedainv  18332  yonffthlem  18333  prdsidlem  18822  mhmvlin  18854  pwsco1mhm  18886  pwsco2mhm  18887  frmdup3lem  18920  frmdup3  18921  grpinvcnv  19068  pwsinvg  19114  pwssub  19115  efginvrel1  19793  frgpup3lem  19842  frgpup3  19843  gsumval3  19972  gsumcllem  19973  gsumzf1o  19977  gsumzsplit  19992  gsumconst  19999  gsumzmhm  20002  gsumsub  20013  gsum2dlem2  20036  gsumcom2  20040  dprdfadd  20087  dprdfsub  20088  dprdfeq0  20089  dprdf11  20090  dmdprdsplitlem  20104  dprddisj2  20106  dpjidcl  20125  ablfaclem2  20153  ablfac2  20156  rrgsupp  20800  mptscmfsuppd  21049  lmhmvsca  21166  mulgrhm2  21628  cygznlem2a  21717  frgpcyg  21723  uvcresum  21943  frlmup1  21948  gsumbagdiaglem  22081  psrass1lem  22083  psrlinv  22105  psrass1  22113  psrcom  22117  mplsubrglem  22153  mplmonmul  22187  mplcoe1  22188  mplcoe5  22191  evlslem2  22230  evlslem6  22232  evlslem1  22233  selvvvval  22293  mhpmulcl  22312  psdmplcl  22325  psdmul  22329  coe1fval3  22368  coe1sclmul  22443  coe1sclmul2  22445  grpvrinv  22556  mdetleib2  22745  mdetunilem9  22777  cayleyhamilton1  23049  neiptopnei  23289  dfac14  23775  ptcnp  23779  lmcn2  23806  cnmpt11f  23821  cnmpt21f  23829  cnmpt2k  23845  qtopeu  23873  xkocnv  23971  xkohmeo  23972  flfcnp2  24164  istgp2  24248  tmdgsum  24252  subgtgp  24262  symgtgp  24263  tgpconncomp  24270  prdstgpd  24282  tsmssub  24306  tgptsmscls  24307  tsmssplit  24309  tsmsxplem1  24310  tlmtgp  24353  ustuqtop  24403  prdsmslem1  24684  prdsxmslem1  24685  prdsxmslem2  24686  tngnm  24808  nmoeq0  24893  cnfldnm  24935  cncfmpt1f  25073  negfcncf  25082  cnrehmeo  25112  evth  25118  evth2  25119  copco  25177  pcopt  25181  pcopt2  25182  pcoass  25183  pcorev2  25187  pi1xfrcnv  25216  ovolctb  25649  ovolfs2  25730  uniioombllem2  25742  ismbf  25787  mbfconst  25792  mbfmulc2re  25807  mbfadd  25820  mbfsub  25821  mbflimsup  25825  mbfi1flimlem  25881  mbfi1flim  25882  mbfmul  25885  itg2uba  25902  itg2mulclem  25905  itg2mulc  25906  itg2splitlem  25907  itg2monolem1  25909  itg2i1fseq  25914  itg2gt0  25919  itg2cnlem1  25920  itg2cnlem2  25921  i1fibl  25967  itgitg1  25968  bddmulibl  25998  bddiblnc  26001  cnplimc  26046  limccnp2  26051  dvcnp2  26079  dvmulf  26102  dvcmulf  26104  dvcobr  26105  dvcof  26107  dvcj  26109  dvfre  26110  dvmptcj  26127  dvcnvlem  26135  dvcnv  26136  dvef  26139  dvsincos  26140  rolle  26149  cmvth  26150  dvlip  26152  dvlipcn  26153  dv11cn  26160  dvivthlem1  26167  dvivth  26169  lhop2  26174  dvfsumrlim2  26191  ftc1lem1  26194  ftc1lem2  26195  ftc1a  26196  ftc1lem4  26198  ftc2  26203  ftc2ditglem  26204  ftc2ditg  26205  tdeglem4  26217  tdeglem2  26218  mdegle0  26234  mdegmullem  26235  plypf1  26369  plyco  26398  dgrcolem1  26430  dgrcolem2  26431  dgrco  26432  plycjlem  26433  plyn0mulidp  26442  dvply2g  26446  plydiveu  26459  elqaalem3  26482  taylthlem1  26536  taylthlem2  26537  ulmshft  26553  ulmdvlem1  26563  mtest  26567  mtestbdd  26568  mbfulm  26569  iblulm  26570  itgulm  26571  pserulm  26585  pserdv  26592  abelthlem1  26594  abelthlem3  26596  pige3ALT  26685  eff1olem  26713  logcn  26812  advlog  26819  advlogexp  26820  logtayl  26825  logccv  26828  dvcxp1  26905  dvcxp2  26906  dvcncxp1  26908  resqrtcn  26914  sqrtcn  26915  loglesqrt  26926  dvatan  27100  leibpi  27107  divsqrtsumo1  27148  jensenlem2  27152  amgmlem  27154  lgamgulmlem2  27194  ftalem7  27243  basellem9  27253  muinv  27357  dchrmullid  27416  dchrinvcl  27417  dchrisum0lem2a  27681  logdivsum  27697  mulog2sumlem1  27698  log2sumbnd  27708  hilnormi  31515  chscllem4  31992  hmopidmchi  32503  rabfodom  32851  ofoprabco  33009  fpwrelmapffslem  33077  fpwrelmap  33078  prodindf  33182  gsummulsubdishift1  33388  gsumwrd2dccat  33398  elrgspn  33566  elrgspnsubrunlem2  33568  domnprodeq0  33599  deg1prod  33873  selvply1rhmlem2  33911  selvply1rhmlem4  33913  selvply1rhm0  33916  mplmulmvr  33929  evlextv  33932  mplvrpmfgalem  33934  mplvrpmga  33935  mplvrpmrhm  33937  psrgsum  33938  psrmonmul  33940  psrmonprod  33942  issply  33951  esplyfval0  33954  esplyfvaln  33964  lbsdiflsp0  34016  fedgmullem1  34019  extdgfialglem2  34083  qqhre  34410  esumpcvgval  34468  ofcfval4  34495  omssubadd  34690  carsggect  34708  fdvneggt  34987  fdvnegge  34989  itgexpif  34993  ptpconn  35725  cvmliftlem6  35782  cvmliftlem8  35784  cvmlift2lem7  35801  cvmliftphtlem  35809  cvmlift3lem5  35815  elmsubrn  36020  knoppcnlem9  37090  curunc  38253  poimir  38304  broucube  38305  mblfinlem2  38309  volsupnfl  38316  cnambfre  38319  dvtan  38321  itg2addnclem  38322  itg2addnclem2  38323  itg2addnclem3  38324  itg2addnc  38325  itg2gt0cn  38326  itgaddnc  38331  itgmulc2nc  38339  ftc1cnnclem  38342  ftc1anclem1  38344  ftc1anclem2  38345  ftc1anclem3  38346  ftc1anclem4  38347  ftc1anclem5  38348  ftc1anclem6  38349  ftc1anclem7  38350  ftc1anclem8  38351  ftc1anc  38352  ftc2nc  38353  upixp  38380  readvcot  43125  evlselv  43321  fsuppssindlem1  43323  fsuppssindlem2  43324  mhphflem  43328  mhphf  43329  mzpsubst  43479  diophun  43504  mendlmod  43916  mendassa  43917  cantnf2  44052  fsovcnvlem  44739  binomcxplemnotnn0  45066  rnsnf  45902  cncfmptss  46303  climliminflimsupd  46515  mulcncff  46584  subcncff  46594  cncfcompt  46597  addcncff  46598  divcncff  46605  cncfiooicclem1  46607  dvsinexp  46625  dvsubf  46628  dvdivf  46636  dvcosax  46640  dvnmul  46657  dvnprodlem1  46660  dvnprodlem2  46661  itgsinexplem1  46668  itgsubsticclem  46689  iblcncfioo  46692  itgiccshift  46694  stoweidlem20  46734  dirkercncflem2  46818  fourierdlem16  46837  fourierdlem21  46842  fourierdlem22  46843  fourierdlem28  46849  fourierdlem39  46860  fourierdlem51  46871  fourierdlem60  46880  fourierdlem61  46881  fourierdlem69  46889  fourierdlem72  46892  fourierdlem73  46893  fourierdlem81  46901  fourierdlem83  46903  fourierdlem84  46904  fourierdlem87  46907  fourierdlem90  46910  fourierdlem93  46913  fourierdlem95  46915  fourierdlem101  46921  fourierdlem103  46923  fourierdlem104  46924  fourierdlem111  46931  etransclem34  46982  etransclem43  46991  etransclem46  46994  sge0tsms  47094  sge0fodjrnlem  47130  sge0iun  47133  sge0isum  47141  sge0seq  47160  meadjun  47176  meadjiunlem  47179  meadjiun  47180  ismeannd  47181  psmeasurelem  47184  omeiunle  47231  ovn02  47282  smfpimioo  47501  smfresal  47502  smfinflem  47531  smflimsuplem3  47536  smfliminflem  47544  1arymaptfo  49423  diag1  50082  aacllem  50621  amgmwlem  50622  amgmlemALT  50623