Theorem feqmptd 6930

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

Syntax hints:   → wi 4   = wceq 1559   ↦ cmpt 5178   Fn wfn 6511  ⟶wf 6512  ‘cfv 6516

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-sep 5243  ax-nul 5253  ax-pr 5387

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-nf 1803  df-sb 2090  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3076  df-rex 3086  df-rab 3414  df-v 3455  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4284  df-if 4478  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4863  df-br 5098  df-opab 5160  df-mpt 5179  df-id 5538  df-xp 5649  df-rel 5650  df-cnv 5651  df-co 5652  df-dm 5653  df-iota 6472  df-fun 6518  df-fn 6519  df-f 6520  df-fv 6524

This theorem is referenced by:  feqresmpt  6931  cofmpt  7109  fcoconst  7111  ofco  7680  caofinvl  7687  caofcom  7692  caofidlcan  7693  caofass  7695  caofdi  7697  caofdir  7698  caonncan  7699  suppssof1  8173  mapxpen  9109  xpmapenlem  9110  cantnfp1  9630  cantnflem1  9638  cnfcom2lem  9650  infxpenc  9968  pwfseqlem5  10615  gruf  10763  ccatco  14842  cnrecnv  15183  rlimclim1  15563  rlimuni  15568  lo1resb  15582  rlimresb  15583  o1resb  15584  rlimcn1  15606  rlimo1  15635  o1rlimmul  15637  caucvgr  15694  ackbijnn  15849  bitsf1ocnv  16469  ramcl  17056  pwsplusgval  17511  pwsmulrval  17512  pwsvscafval  17515  setcepi  18112  prf1st  18227  prf2nd  18228  1st2ndprf  18229  curfuncf  18261  curf2ndf  18270  yonedainv  18304  yonffthlem  18305  prdsidlem  18794  mhmvlin  18826  pwsco1mhm  18857  pwsco2mhm  18858  frmdup3lem  18891  frmdup3  18892  grpinvcnv  19039  pwsinvg  19086  pwssub  19087  efginvrel1  19759  frgpup3lem  19808  frgpup3  19809  gsumval3  19938  gsumcllem  19939  gsumzf1o  19943  gsumzsplit  19958  gsumconst  19965  gsumzmhm  19968  gsumsub  19979  gsum2dlem2  20002  gsumcom2  20006  dprdfadd  20053  dprdfsub  20054  dprdfeq0  20055  dprdf11  20056  dmdprdsplitlem  20070  dprddisj2  20072  dpjidcl  20091  ablfaclem2  20119  ablfac2  20122  rrgsupp  20738  mptscmfsuppd  20983  lmhmvsca  21100  mulgrhm2  21518  cygznlem2a  21607  frgpcyg  21613  uvcresum  21833  frlmup1  21838  gsumbagdiaglem  21971  psrass1lem  21973  psrlinv  21995  psrass1  22003  psrcom  22007  mplsubrglem  22043  mplmonmul  22077  mplcoe1  22078  mplcoe5  22081  evlslem2  22120  evlslem6  22122  evlslem1  22123  selvvvval  22183  mhpmulcl  22202  psdmplcl  22215  psdmul  22219  coe1fval3  22258  coe1sclmul  22333  coe1sclmul2  22335  grpvrinv  22447  mdetleib2  22636  mdetunilem9  22668  cayleyhamilton1  22940  neiptopnei  23180  dfac14  23666  ptcnp  23670  lmcn2  23697  cnmpt11f  23712  cnmpt21f  23720  cnmpt2k  23736  qtopeu  23764  xkocnv  23862  xkohmeo  23863  flfcnp2  24055  istgp2  24139  tmdgsum  24143  subgtgp  24153  symgtgp  24154  tgpconncomp  24161  prdstgpd  24173  tsmssub  24197  tgptsmscls  24198  tsmssplit  24200  tsmsxplem1  24201  tlmtgp  24244  ustuqtop  24294  prdsmslem1  24575  prdsxmslem1  24576  prdsxmslem2  24577  tngnm  24699  nmoeq0  24784  cnfldnm  24826  cncfmpt1f  24964  negfcncf  24973  cnrehmeo  25003  evth  25009  evth2  25010  copco  25068  pcopt  25072  pcopt2  25073  pcoass  25074  pcorev2  25078  pi1xfrcnv  25107  ovolctb  25540  ovolfs2  25621  uniioombllem2  25633  ismbf  25678  mbfconst  25683  mbfmulc2re  25698  mbfadd  25711  mbfsub  25712  mbflimsup  25716  mbfi1flimlem  25772  mbfi1flim  25773  mbfmul  25776  itg2uba  25793  itg2mulclem  25796  itg2mulc  25797  itg2splitlem  25798  itg2monolem1  25800  itg2i1fseq  25805  itg2gt0  25810  itg2cnlem1  25811  itg2cnlem2  25812  i1fibl  25858  itgitg1  25859  bddmulibl  25889  bddiblnc  25892  cnplimc  25937  limccnp2  25942  dvcnp2  25970  dvmulf  25993  dvcmulf  25995  dvcobr  25996  dvcof  25998  dvcj  26000  dvfre  26001  dvmptcj  26018  dvcnvlem  26026  dvcnv  26027  dvef  26030  dvsincos  26031  rolle  26040  cmvth  26041  dvlip  26043  dvlipcn  26044  dv11cn  26051  dvivthlem1  26058  dvivth  26060  lhop2  26065  dvfsumrlim2  26082  ftc1lem1  26085  ftc1lem2  26086  ftc1a  26087  ftc1lem4  26089  ftc2  26094  ftc2ditglem  26095  ftc2ditg  26096  tdeglem4  26108  tdeglem2  26109  mdegle0  26125  mdegmullem  26126  plypf1  26260  plyco  26289  dgrcolem1  26321  dgrcolem2  26322  dgrco  26323  plycjlem  26324  plyn0mulidp  26333  dvply2g  26337  plydiveu  26350  elqaalem3  26373  taylthlem1  26424  taylthlem2  26425  ulmshft  26441  ulmdvlem1  26451  mtest  26455  mtestbdd  26456  mbfulm  26457  iblulm  26458  itgulm  26459  pserulm  26473  pserdv  26480  abelthlem1  26482  abelthlem3  26484  pige3ALT  26573  eff1olem  26601  logcn  26700  advlog  26707  advlogexp  26708  logtayl  26713  logccv  26716  dvcxp1  26793  dvcxp2  26794  dvcncxp1  26796  resqrtcn  26802  sqrtcn  26803  loglesqrt  26814  dvatan  26988  leibpi  26995  divsqrtsumo1  27036  jensenlem2  27040  amgmlem  27042  lgamgulmlem2  27082  ftalem7  27131  basellem9  27141  muinv  27245  dchrmullid  27304  dchrinvcl  27305  dchrisum0lem2a  27569  logdivsum  27585  mulog2sumlem1  27586  log2sumbnd  27596  hilnormi  31323  chscllem4  31800  hmopidmchi  32311  rabfodom  32664  ofoprabco  32827  fpwrelmapffslem  32895  fpwrelmap  32896  prodindf  33001  gsummulsubdishift1  33209  gsumwrd2dccat  33219  elrgspn  33388  elrgspnsubrunlem2  33390  domnprodeq0  33421  deg1prod  33740  selvply1rhmlem2  33779  selvply1rhmlem4  33781  selvply1rhm0  33784  mplmulmvr  33797  evlextv  33800  mplvrpmfgalem  33802  mplvrpmga  33803  mplvrpmrhm  33805  psrgsum  33806  psrmonmul  33808  psrmonprod  33810  issply  33819  esplyfval0  33822  esplyfvaln  33832  lbsdiflsp0  33884  fedgmullem1  33887  extdgfialglem2  33951  qqhre  34278  esumpcvgval  34336  ofcfval4  34363  omssubadd  34558  carsggect  34576  fdvneggt  34855  fdvnegge  34857  itgexpif  34861  ptpconn  35544  cvmliftlem6  35601  cvmliftlem8  35603  cvmlift2lem7  35620  cvmliftphtlem  35628  cvmlift3lem5  35634  elmsubrn  35839  knoppcnlem9  36900  curunc  38062  poimir  38113  broucube  38114  mblfinlem2  38118  volsupnfl  38125  cnambfre  38128  dvtan  38130  itg2addnclem  38131  itg2addnclem2  38132  itg2addnclem3  38133  itg2addnc  38134  itg2gt0cn  38135  itgaddnc  38140  itgmulc2nc  38148  ftc1cnnclem  38151  ftc1anclem1  38153  ftc1anclem2  38154  ftc1anclem3  38155  ftc1anclem4  38156  ftc1anclem5  38157  ftc1anclem6  38158  ftc1anclem7  38159  ftc1anclem8  38160  ftc1anc  38161  ftc2nc  38162  upixp  38189  readvcot  42934  evlselv  43132  fsuppssindlem1  43134  fsuppssindlem2  43135  mhphflem  43139  mhphf  43140  mzpsubst  43290  diophun  43315  mendlmod  43727  mendassa  43728  cantnf2  43863  fsovcnvlem  44550  binomcxplemnotnn0  44893  rnsnf  45723  cncfmptss  46124  climliminflimsupd  46336  mulcncff  46405  subcncff  46415  cncfcompt  46418  addcncff  46419  divcncff  46426  cncfiooicclem1  46428  dvsinexp  46446  dvsubf  46449  dvdivf  46457  dvcosax  46461  dvnmul  46478  dvnprodlem1  46481  dvnprodlem2  46482  itgsinexplem1  46489  itgsubsticclem  46510  iblcncfioo  46513  itgiccshift  46515  stoweidlem20  46555  dirkercncflem2  46639  fourierdlem16  46658  fourierdlem21  46663  fourierdlem22  46664  fourierdlem28  46670  fourierdlem39  46681  fourierdlem51  46692  fourierdlem60  46701  fourierdlem61  46702  fourierdlem69  46710  fourierdlem72  46713  fourierdlem73  46714  fourierdlem81  46722  fourierdlem83  46724  fourierdlem84  46725  fourierdlem87  46728  fourierdlem90  46731  fourierdlem93  46734  fourierdlem95  46736  fourierdlem101  46742  fourierdlem103  46744  fourierdlem104  46745  fourierdlem111  46752  etransclem34  46803  etransclem43  46812  etransclem46  46815  sge0tsms  46915  sge0fodjrnlem  46951  sge0iun  46954  sge0isum  46962  sge0seq  46981  meadjun  46997  meadjiunlem  47000  meadjiun  47001  ismeannd  47002  psmeasurelem  47005  omeiunle  47052  ovn02  47103  smfpimioo  47322  smfresal  47323  smfinflem  47352  smflimsuplem3  47357  smfliminflem  47365  1arymaptfo  49226  diag1  49886  aacllem  50383  amgmwlem  50384  amgmlemALT  50385