Theorem feqmptd 6984

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ↦ cmpt 5192   Fn wfn 6561  ⟶wf 6562  ‘cfv 6566

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5255  ax-nul 5266  ax-pr 5398

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4841  df-uni 4873  df-br 5109  df-opab 5174  df-mpt 5193  df-id 5553  df-xp 5664  df-rel 5665  df-cnv 5666  df-co 5667  df-dm 5668  df-iota 6520  df-fun 6568  df-fn 6569  df-f 6570  df-fv 6574

This theorem is used by:  feqresmpt  6985  cofmpt  7165  fcoconst  7167  ofco  7750  caofinvl  7757  caofcom  7762  caofidlcan  7763  caofass  7765  caofdi  7767  caofdir  7768  caonncan  7769  suppssof1  8254  mapxpen  9200  xpmapenlem  9201  cantnfp1  9719  cantnflem1  9727  cnfcom2lem  9739  infxpenc  10136  pwfseqlem5  10787  gruf  10935  ccatco  15028  cnrecnv  15375  rlimclim1  15756  rlimuni  15761  lo1resb  15775  rlimresb  15776  o1resb  15777  rlimcn1  15799  rlimo1  15828  o1rlimmul  15830  caucvgr  15887  ackbijnn  16041  bitsf1ocnv  16658  ramcl  17251  pwsplusgval  17712  pwsmulrval  17713  pwsvscafval  17716  setcepi  18313  prf1st  18428  prf2nd  18429  1st2ndprf  18430  curfuncf  18462  curf2ndf  18471  yonedainv  18505  yonffthlem  18506  prdsidlem  19013  mhmvlin  19046  pwsco1mhm  19078  pwsco2mhm  19079  frmdup3lem  19112  frmdup3  19113  grpinvcnv  19267  pwsinvg  19313  pwssub  19314  efginvrel1  19993  frgpup3lem  20042  frgpup3  20043  gsumval3  20172  gsumcllem  20173  gsumzf1o  20177  gsumzsplit  20192  gsumconst  20199  gsumzmhm  20202  gsumsub  20213  gsum2dlem2  20236  gsumcom2  20240  dprdfadd  20287  dprdfsub  20288  dprdfeq0  20289  dprdf11  20290  dmdprdsplitlem  20304  dprddisj2  20306  dpjidcl  20325  ablfaclem2  20353  ablfac2  20356  rrgsupp  21004  mptscmfsuppd  21254  lmhmvsca  21371  mulgrhm2  21839  cygznlem2a  21928  frgpcyg  21934  uvcresum  22154  frlmup1  22159  gsumbagdiaglem  22294  psrass1lem  22296  psrlinv  22318  psrass1  22326  psrcom  22330  mplsubrglem  22366  mplmonmul  22400  mplcoe1  22401  mplcoe5  22404  evlslem2  22443  evlslem6  22445  evlslem1  22446  selvvvval  22506  mhpmulcl  22525  psdmplcl  22538  psdmul  22542  coe1fval3  22581  coe1sclmul  22656  coe1sclmul2  22658  grpvrinv  22769  mdetleib2  22958  mdetunilem9  22990  cayleyhamilton1  23265  neiptopnei  23505  dfac14  23992  ptcnp  23996  lmcn2  24023  cnmpt11f  24038  cnmpt21f  24046  cnmpt2k  24062  qtopeu  24090  xkocnv  24188  xkohmeo  24189  flfcnp2  24381  istgp2  24465  tmdgsum  24469  subgtgp  24479  symgtgp  24480  tgpconncomp  24487  prdstgpd  24499  tsmssub  24523  tgptsmscls  24524  tsmssplit  24526  tsmsxplem1  24527  tlmtgp  24570  ustuqtop  24620  prdsmslem1  24901  prdsxmslem1  24902  prdsxmslem2  24903  tngnm  25025  nmoeq0  25110  cnfldnm  25152  cncfmpt1f  25290  negfcncf  25299  cnrehmeo  25329  evth  25335  evth2  25336  copco  25394  pcopt  25398  pcopt2  25399  pcoass  25400  pcorev2  25404  pi1xfrcnv  25433  ovolctb  25866  ovolfs2  25947  uniioombllem2  25959  ismbf  26004  mbfconst  26009  mbfmulc2re  26024  mbfadd  26037  mbfsub  26038  mbflimsup  26042  mbfi1flimlem  26098  mbfi1flim  26099  mbfmul  26102  itg2uba  26119  itg2mulclem  26122  itg2mulc  26123  itg2splitlem  26124  itg2monolem1  26126  itg2i1fseq  26131  itg2gt0  26136  itg2cnlem1  26137  itg2cnlem2  26138  i1fibl  26183  itgitg1  26184  bddmulibl  26214  bddiblnc  26217  cnplimc  26262  limccnp2  26267  dvcnp2  26295  dvmulf  26318  dvcmulf  26320  dvcobr  26321  dvcof  26323  dvcj  26325  dvfre  26326  dvmptcj  26343  dvcnvlem  26351  dvcnv  26352  dvef  26355  dvsincos  26356  rolle  26365  cmvth  26366  dvlip  26368  dvlipcn  26369  dv11cn  26376  dvivthlem1  26383  dvivth  26385  lhop2  26390  dvfsumrlim2  26407  ftc1lem1  26410  ftc1lem2  26411  ftc1a  26412  ftc1lem4  26414  ftc2  26419  ftc2ditglem  26420  ftc2ditg  26421  tdeglem4  26433  tdeglem2  26434  mdegle0  26450  mdegmullem  26451  plypf1  26586  plyco  26615  dgrcolem1  26647  dgrcolem2  26648  dgrco  26649  plycjlem  26650  plyn0mulidp  26657  dvply2g  26661  plydiveu  26674  elqaalem3  26701  taylthlem1  26757  taylthlem2  26758  ulmshft  26774  ulmdvlem1  26784  mtest  26788  mtestbdd  26789  mbfulm  26790  iblulm  26791  itgulm  26792  pserulm  26806  pserdv  26813  abelthlem1  26815  abelthlem3  26817  pige3ALT  26905  eff1olem  26933  logcn  27032  advlog  27039  advlogexp  27040  logtayl  27045  logccv  27048  dvcxp1  27125  dvcxp2  27126  dvcncxp1  27128  resqrtcn  27134  sqrtcn  27135  loglesqrt  27146  dvatan  27320  leibpi  27327  divsqrtsumo1  27368  jensenlem2  27372  amgmlem  27374  lgamgulmlem2  27414  ftalem7  27463  basellem9  27473  muinv  27577  dchrmullid  27636  dchrinvcl  27637  dchrisum0lem2a  27901  logdivsum  27917  mulog2sumlem1  27918  log2sumbnd  27928  hilnormi  31822  chscllem4  32299  hmopidmchi  32810  rabfodom  33200  ofoprabco  33356  fpwrelmapffslem  33420  fpwrelmap  33421  prodindf  33525  gsummulsubdishift1  33728  gsumwrd2dccat  33738  elrgspn  33906  elrgspnsubrunlem2  33908  domnprodeq0  33939  deg1prod  34218  selvply1rhmlem2  34264  selvply1rhmlem4  34266  selvply1rhm0  34269  mplmulmvr  34282  evlextv  34285  mplvrpmfgalem  34287  mplvrpmga  34288  mplvrpmrhm  34290  psrgsum  34291  psrmonmul  34293  psrmonprod  34295  issply  34304  esplyfval0  34307  esplyfvaln  34317  lbsdiflsp0  34369  fedgmullem1  34372  extdgfialglem2  34436  qqhre  34763  esumpcvgval  34821  ofcfval4  34848  omssubadd  35043  carsggect  35061  fdvneggt  35340  fdvnegge  35342  itgexpif  35346  ptpconn  36206  cvmliftlem6  36263  cvmliftlem8  36265  cvmlift2lem7  36282  cvmliftphtlem  36290  cvmlift3lem5  36296  elmsubrn  36501  knoppcnlem9  37582  curunc  38793  poimir  38839  broucube  38840  mblfinlem2  38844  volsupnfl  38851  cnambfre  38854  dvtan  38856  itg2addnclem  38857  itg2addnclem2  38858  itg2addnclem3  38859  itg2addnc  38860  itg2gt0cn  38861  itgaddnc  38866  itgmulc2nc  38874  ftc1cnnclem  38877  ftc1anclem1  38879  ftc1anclem2  38880  ftc1anclem3  38881  ftc1anclem4  38882  ftc1anclem5  38883  ftc1anclem6  38884  ftc1anclem7  38885  ftc1anclem8  38886  ftc1anc  38887  ftc2nc  38888  upixp  38931  readvcot  43681  evlselv  43883  fsuppssindlem1  43885  fsuppssindlem2  43886  mhphflem  43890  mhphf  43891  mzpsubst  44025  diophun  44050  mendlmod  44452  mendassa  44453  cantnf2  44588  fsovcnvlem  45274  binomcxplemnotnn0  45601  rnsnf  46472  cncfmptss  46872  climliminflimsupd  47084  mulcncff  47153  subcncff  47163  cncfcompt  47166  addcncff  47167  divcncff  47174  cncfiooicclem1  47176  dvsinexp  47194  dvsubf  47197  dvdivf  47205  dvcosax  47209  dvnmul  47226  dvnprodlem1  47229  dvnprodlem2  47230  itgsinexplem1  47237  itgsubsticclem  47258  iblcncfioo  47261  itgiccshift  47263  stoweidlem20  47303  dirkercncflem2  47387  fourierdlem16  47406  fourierdlem21  47411  fourierdlem22  47412  fourierdlem28  47418  fourierdlem39  47429  fourierdlem51  47440  fourierdlem60  47449  fourierdlem61  47450  fourierdlem69  47458  fourierdlem72  47461  fourierdlem73  47462  fourierdlem81  47470  fourierdlem83  47472  fourierdlem84  47473  fourierdlem87  47476  fourierdlem90  47479  fourierdlem93  47482  fourierdlem95  47484  fourierdlem101  47490  fourierdlem103  47492  fourierdlem104  47493  fourierdlem111  47500  etransclem34  47551  etransclem43  47560  etransclem46  47563  sge0tsms  47663  sge0fodjrnlem  47699  sge0iun  47702  sge0isum  47710  sge0seq  47729  meadjun  47745  meadjiunlem  47748  meadjiun  47749  ismeannd  47750  psmeasurelem  47753  omeiunle  47800  ovn02  47851  smfpimioo  48070  smfresal  48071  smfinflem  48100  smflimsuplem3  48105  smfliminflem  48113  1arymaptfo  50086  diag1  50757  dvsec  51284  dvcsc  51285  dvcot  51286  aacllem  51367  amgmwlem  51415  amgmlemALT  51416