Theorem feqmptd 6976

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

Syntax hints:   → wi 4   = wceq 1536   ↦ cmpt 5230   Fn wfn 6557  ⟶wf 6558  ‘cfv 6562

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pr 5437

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-ral 3059  df-rex 3068  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5582  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-fv 6570

This theorem is referenced by:  feqresmpt  6977  cofmpt  7151  fcoconst  7153  ofco  7721  caofinvl  7728  caofcom  7733  caofass  7735  caofdi  7737  caofdir  7738  caonncan  7739  suppssof1  8222  mapxpen  9181  xpmapenlem  9182  cantnfp1  9718  cantnflem1  9726  cnfcom2lem  9738  infxpenc  10055  pwfseqlem5  10700  gruf  10848  ccatco  14870  cnrecnv  15200  rlimclim1  15577  rlimuni  15582  lo1resb  15596  rlimresb  15597  o1resb  15598  rlimcn1  15620  rlimo1  15649  o1rlimmul  15651  caucvgr  15708  ackbijnn  15860  bitsf1ocnv  16477  ramcl  17062  pwsplusgval  17536  pwsmulrval  17537  pwsvscafval  17540  setcepi  18141  prf1st  18259  prf2nd  18260  1st2ndprf  18261  curfuncf  18294  curf2ndf  18303  yonedainv  18337  yonffthlem  18338  prdsidlem  18794  mhmvlin  18826  pwsco1mhm  18857  pwsco2mhm  18858  frmdup3lem  18891  frmdup3  18892  grpinvcnv  19036  pwsinvg  19083  pwssub  19084  efginvrel1  19760  frgpup3lem  19809  frgpup3  19810  gsumval3  19939  gsumcllem  19940  gsumzf1o  19944  gsumzsplit  19959  gsumconst  19966  gsumzmhm  19969  gsumsub  19980  gsum2dlem2  20003  gsumcom2  20007  dprdfadd  20054  dprdfsub  20055  dprdfeq0  20056  dprdf11  20057  dmdprdsplitlem  20071  dprddisj2  20073  dpjidcl  20092  ablfaclem2  20120  ablfac2  20123  rrgsupp  20717  mptscmfsuppd  20942  lmhmvsca  21061  mulgrhm2  21506  cygznlem2a  21603  frgpcyg  21609  uvcresum  21830  frlmup1  21835  gsumbagdiaglem  21967  psrass1lem  21969  psrlinv  21992  psrass1  22001  psrcom  22005  mplsubrglem  22041  mplmonmul  22071  mplcoe1  22072  mplcoe5  22075  evlslem2  22120  evlslem6  22122  evlslem1  22123  mhpmulcl  22170  psdmplcl  22183  psdmul  22187  coe1fval3  22225  coe1sclmul  22300  coe1sclmul2  22302  grpvrinv  22418  mdetleib2  22609  mdetunilem9  22641  cayleyhamilton1  22913  neiptopnei  23155  dfac14  23641  ptcnp  23645  lmcn2  23672  cnmpt11f  23687  cnmpt21f  23695  cnmpt2k  23711  qtopeu  23739  xkocnv  23837  xkohmeo  23838  flfcnp2  24030  istgp2  24114  tmdgsum  24118  subgtgp  24128  symgtgp  24129  tgpconncomp  24136  prdstgpd  24148  tsmssub  24172  tgptsmscls  24173  tsmssplit  24175  tsmsxplem1  24176  tlmtgp  24219  ustuqtop  24270  prdsmslem1  24555  prdsxmslem1  24556  prdsxmslem2  24557  tngnm  24687  nmoeq0  24772  cnfldnm  24814  cncfmpt1f  24953  negfcncf  24963  cnrehmeo  24997  cnrehmeoOLD  24998  evth  25004  evth2  25005  copco  25064  pcopt  25068  pcopt2  25069  pcoass  25070  pcorev2  25074  pi1xfrcnv  25103  ovolctb  25538  ovolfs2  25619  uniioombllem2  25631  ismbf  25676  mbfconst  25681  mbfmulc2re  25696  mbfadd  25709  mbfsub  25710  mbflimsup  25714  mbfi1flimlem  25771  mbfi1flim  25772  mbfmul  25775  itg2uba  25792  itg2mulclem  25795  itg2mulc  25796  itg2splitlem  25797  itg2monolem1  25799  itg2i1fseq  25804  itg2gt0  25809  itg2cnlem1  25810  itg2cnlem2  25811  i1fibl  25857  itgitg1  25858  bddmulibl  25888  bddiblnc  25891  cnplimc  25936  limccnp2  25941  dvcnp2  25969  dvcnp2OLD  25970  dvmulf  25994  dvcmulf  25996  dvcobr  25997  dvcobrOLD  25998  dvcof  26000  dvcj  26002  dvfre  26003  dvmptcj  26020  dvcnvlem  26028  dvcnv  26029  dvef  26032  dvsincos  26033  rolle  26042  cmvth  26043  cmvthOLD  26044  dvlip  26046  dvlipcn  26047  dv11cn  26054  dvivthlem1  26061  dvivth  26063  lhop2  26068  dvfsumrlim2  26087  ftc1lem1  26090  ftc1lem2  26091  ftc1a  26092  ftc1lem4  26094  ftc2  26099  ftc2ditglem  26100  ftc2ditg  26101  tdeglem4  26113  tdeglem2  26114  mdegle0  26130  mdegmullem  26131  plypf1  26265  plyco  26294  dgrcolem1  26327  dgrcolem2  26328  dgrco  26329  plycjlem  26330  dvply2g  26340  dvply2gOLD  26341  plydiveu  26354  elqaalem3  26377  taylthlem1  26429  taylthlem2  26430  taylthlem2OLD  26431  ulmshft  26447  ulmdvlem1  26457  mtest  26461  mtestbdd  26462  mbfulm  26463  iblulm  26464  itgulm  26465  pserulm  26479  pserdv  26487  abelthlem1  26489  abelthlem3  26491  pige3ALT  26576  eff1olem  26604  logcn  26703  advlog  26710  advlogexp  26711  logtayl  26716  logccv  26719  dvcxp1  26796  dvcxp2  26797  dvcncxp1  26799  resqrtcn  26806  sqrtcn  26807  loglesqrt  26818  dvatan  26992  leibpi  26999  divsqrtsumo1  27041  jensenlem2  27045  amgmlem  27047  lgamgulmlem2  27087  ftalem7  27136  basellem9  27146  muinv  27250  dchrmullid  27310  dchrinvcl  27311  dchrisum0lem2a  27575  logdivsum  27591  mulog2sumlem1  27592  log2sumbnd  27602  hilnormi  31191  chscllem4  31668  hmopidmchi  32179  rabfodom  32532  ofoprabco  32680  fpwrelmapffslem  32749  fpwrelmap  32750  gsumwrd2dccat  33052  lbsdiflsp0  33653  fedgmullem1  33656  qqhre  33982  prodindf  34003  esumpcvgval  34058  ofcfval4  34085  omssubadd  34281  carsggect  34299  plymulx0  34540  fdvneggt  34593  fdvnegge  34595  itgexpif  34599  ptpconn  35217  cvmliftlem6  35274  cvmliftlem8  35276  cvmlift2lem7  35293  cvmliftphtlem  35301  cvmlift3lem5  35307  elmsubrn  35512  knoppcnlem9  36483  curunc  37588  poimir  37639  broucube  37640  mblfinlem2  37644  volsupnfl  37651  cnambfre  37654  dvtan  37656  itg2addnclem  37657  itg2addnclem2  37658  itg2addnclem3  37659  itg2addnc  37660  itg2gt0cn  37661  itgaddnc  37666  itgmulc2nc  37674  ftc1cnnclem  37677  ftc1anclem1  37679  ftc1anclem2  37680  ftc1anclem3  37681  ftc1anclem4  37682  ftc1anclem5  37683  ftc1anclem6  37684  ftc1anclem7  37685  ftc1anclem8  37686  ftc1anc  37687  ftc2nc  37688  upixp  37715  readvrec  42370  selvvvval  42571  evlselv  42573  fsuppssindlem1  42577  fsuppssindlem2  42578  mhphflem  42582  mhphf  42583  mzpsubst  42735  diophun  42760  mendlmod  43177  mendassa  43178  cantnf2  43314  fsovcnvlem  44002  binomcxplemnotnn0  44351  rnsnf  45126  cncfmptss  45542  climliminflimsupd  45756  mulcncff  45825  subcncff  45835  cncfcompt  45838  addcncff  45839  divcncff  45846  cncfiooicclem1  45848  dvsinexp  45866  dvsubf  45869  dvdivf  45877  dvcosax  45881  dvnmul  45898  dvnprodlem1  45901  dvnprodlem2  45902  itgsinexplem1  45909  itgsubsticclem  45930  iblcncfioo  45933  itgiccshift  45935  stoweidlem20  45975  dirkercncflem2  46059  fourierdlem16  46078  fourierdlem21  46083  fourierdlem22  46084  fourierdlem28  46090  fourierdlem39  46101  fourierdlem51  46112  fourierdlem60  46121  fourierdlem61  46122  fourierdlem69  46130  fourierdlem72  46133  fourierdlem73  46134  fourierdlem81  46142  fourierdlem83  46144  fourierdlem84  46145  fourierdlem87  46148  fourierdlem90  46151  fourierdlem93  46154  fourierdlem95  46156  fourierdlem101  46162  fourierdlem103  46164  fourierdlem104  46165  fourierdlem111  46172  etransclem34  46223  etransclem43  46232  etransclem46  46235  sge0tsms  46335  sge0fodjrnlem  46371  sge0iun  46374  sge0isum  46382  sge0seq  46401  meadjun  46417  meadjiunlem  46420  meadjiun  46421  ismeannd  46422  psmeasurelem  46425  omeiunle  46472  ovn02  46523  smfpimioo  46742  smfresal  46743  smfinflem  46772  smflimsuplem3  46777  smfliminflem  46785  1arymaptfo  48492  aacllem  49031  amgmwlem  49032  amgmlemALT  49033