Theorem feqmptd 6735

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

Syntax hints:   → wi 4   = wceq 1537   ↦ cmpt 5148   Fn wfn 6352  ⟶wf 6353  ‘cfv 6357

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795  ax-sep 5205  ax-nul 5212  ax-pr 5332

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-ral 3145  df-rex 3146  df-rab 3149  df-v 3498  df-sbc 3775  df-dif 3941  df-un 3943  df-in 3945  df-ss 3954  df-nul 4294  df-if 4470  df-sn 4570  df-pr 4572  df-op 4576  df-uni 4841  df-br 5069  df-opab 5131  df-mpt 5149  df-id 5462  df-xp 5563  df-rel 5564  df-cnv 5565  df-co 5566  df-dm 5567  df-iota 6316  df-fun 6359  df-fn 6360  df-f 6361  df-fv 6365

This theorem is referenced by:  feqresmpt  6736  cofmpt  6896  fcoconst  6898  ofco  7431  caofinvl  7438  caofcom  7443  caofass  7445  caofdi  7447  caofdir  7448  caonncan  7449  suppssof1  7865  mapxpen  8685  xpmapenlem  8686  cantnfp1  9146  cantnflem1  9154  cnfcom2lem  9166  infxpenc  9446  pwfseqlem5  10087  gruf  10235  ccatco  14199  cnrecnv  14526  rlimclim1  14904  rlimuni  14909  lo1resb  14923  rlimresb  14924  o1resb  14925  rlimcn1  14947  rlimo1  14975  o1rlimmul  14977  caucvgr  15034  ackbijnn  15185  bitsf1ocnv  15795  ramcl  16367  pwsplusgval  16765  pwsmulrval  16766  pwsvscafval  16769  setcepi  17350  prf1st  17456  prf2nd  17457  1st2ndprf  17458  curfuncf  17490  curf2ndf  17499  yonedainv  17533  yonffthlem  17534  prdsidlem  17945  pwsco1mhm  17998  pwsco2mhm  17999  frmdup3lem  18033  frmdup3  18034  grpinvcnv  18169  pwsinvg  18214  pwssub  18215  efginvrel1  18856  frgpup3lem  18905  frgpup3  18906  gsumval3  19029  gsumcllem  19030  gsumzf1o  19034  gsumzsplit  19049  gsumconst  19056  gsumzmhm  19059  gsumsub  19070  gsum2dlem2  19093  gsumcom2  19097  dprdfadd  19144  dprdfsub  19145  dprdfeq0  19146  dprdf11  19147  dmdprdsplitlem  19161  dprddisj2  19163  dpjidcl  19182  ablfaclem2  19210  ablfac2  19213  mptscmfsuppd  19702  lmhmvsca  19819  rrgsupp  20066  psrbagaddcl  20152  gsumbagdiaglem  20157  psrass1lem  20159  psrlinv  20179  psrass1  20187  psrcom  20191  mplsubrglem  20221  mplmonmul  20247  mplcoe1  20248  mplcoe5  20251  evlslem2  20294  evlslem6  20296  evlslem1  20297  coe1fval3  20378  coe1sclmul  20452  coe1sclmul2  20454  mulgrhm2  20648  cygznlem2a  20716  frgpcyg  20722  uvcresum  20939  frlmup1  20944  grpvrinv  21009  mhmvlin  21010  mdetleib2  21199  mdetunilem9  21231  cayleyhamilton1  21502  neiptopnei  21742  dfac14  22228  ptcnp  22232  lmcn2  22259  cnmpt11f  22274  cnmpt21f  22282  cnmpt2k  22298  qtopeu  22326  xkocnv  22424  xkohmeo  22425  flfcnp2  22617  istgp2  22701  tmdgsum  22705  subgtgp  22715  symgtgp  22716  tgpconncomp  22723  prdstgpd  22735  tsmssub  22759  tgptsmscls  22760  tsmssplit  22762  tsmsxplem1  22763  tlmtgp  22806  ustuqtop  22857  prdsmslem1  23139  prdsxmslem1  23140  prdsxmslem2  23141  tngnm  23262  nmoeq0  23347  cnfldnm  23389  cncfmpt1f  23523  negfcncf  23529  cnrehmeo  23559  evth  23565  evth2  23566  copco  23624  pcopt  23628  pcopt2  23629  pcoass  23630  pcorev2  23634  pi1xfrcnv  23663  ovolctb  24093  ovolfs2  24174  uniioombllem2  24186  ismbf  24231  mbfconst  24236  mbfmulc2re  24251  mbfadd  24264  mbfsub  24265  mbflimsup  24269  mbfi1flimlem  24325  mbfi1flim  24326  mbfmul  24329  itg2uba  24346  itg2mulclem  24349  itg2mulc  24350  itg2splitlem  24351  itg2monolem1  24353  itg2i1fseq  24358  itg2gt0  24363  itg2cnlem1  24364  itg2cnlem2  24365  i1fibl  24410  itgitg1  24411  bddmulibl  24441  cnplimc  24487  limccnp2  24492  dvcnp2  24519  dvmulf  24542  dvcmulf  24544  dvcobr  24545  dvcof  24547  dvcj  24549  dvfre  24550  dvmptcj  24567  dvcnvlem  24575  dvcnv  24576  dvef  24579  dvsincos  24580  rolle  24589  cmvth  24590  dvlip  24592  dvlipcn  24593  dv11cn  24600  dvivthlem1  24607  dvivth  24609  lhop2  24614  dvfsumrlim2  24631  ftc1lem1  24634  ftc1lem2  24635  ftc1a  24636  ftc1lem4  24638  ftc2  24643  ftc2ditglem  24644  ftc2ditg  24645  tdeglem4  24656  tdeglem2  24657  mdegle0  24673  mdegmullem  24674  plypf1  24804  plyco  24833  dgrcolem1  24865  dgrcolem2  24866  dgrco  24867  plycjlem  24868  dvply2g  24876  plydiveu  24889  elqaalem3  24912  taylthlem1  24963  taylthlem2  24964  ulmshft  24980  ulmdvlem1  24990  mtest  24994  mtestbdd  24995  mbfulm  24996  iblulm  24997  itgulm  24998  pserulm  25012  pserdv  25019  abelthlem1  25021  abelthlem3  25023  pige3ALT  25107  eff1olem  25134  logcn  25232  advlog  25239  advlogexp  25240  logtayl  25245  logccv  25248  dvcxp1  25323  dvcxp2  25324  dvcncxp1  25326  resqrtcn  25332  sqrtcn  25333  loglesqrt  25341  dvatan  25515  leibpi  25522  divsqrtsumo1  25563  jensenlem2  25567  amgmlem  25569  lgamgulmlem2  25609  ftalem7  25658  basellem9  25668  muinv  25772  dchrmulid2  25830  dchrinvcl  25831  dchrisum0lem2a  26095  logdivsum  26111  mulog2sumlem1  26112  log2sumbnd  26122  hilnormi  28942  chscllem4  29419  hmopidmchi  29930  rabfodom  30268  ofoprabco  30411  fpwrelmapffslem  30470  fpwrelmap  30471  lbsdiflsp0  31024  fedgmullem1  31027  qqhre  31263  prodindf  31284  esumpcvgval  31339  ofcfval4  31366  omssubadd  31560  carsggect  31578  plymulx0  31819  fdvneggt  31873  fdvnegge  31875  itgexpif  31879  ptpconn  32482  cvmliftlem6  32539  cvmliftlem8  32541  cvmlift2lem7  32558  cvmliftphtlem  32566  cvmlift3lem5  32572  elmsubrn  32777  knoppcnlem9  33842  curunc  34876  poimir  34927  broucube  34928  mblfinlem2  34932  volsupnfl  34939  cnambfre  34942  dvtan  34944  itg2addnclem  34945  itg2addnclem2  34946  itg2addnclem3  34947  itg2addnc  34948  itg2gt0cn  34949  itgaddnc  34954  itgmulc2nc  34962  bddiblnc  34964  ftc1cnnclem  34967  ftc1anclem1  34969  ftc1anclem2  34970  ftc1anclem3  34971  ftc1anclem4  34972  ftc1anclem5  34973  ftc1anclem6  34974  ftc1anclem7  34975  ftc1anclem8  34976  ftc1anc  34977  ftc2nc  34978  upixp  35006  mzpsubst  39352  diophun  39377  mendlmod  39800  mendassa  39801  fsovcnvlem  40366  binomcxplemnotnn0  40695  rnsnf  41451  cncfmptss  41875  climliminflimsupd  42089  mulcncff  42158  subcncff  42170  cncfcompt  42173  addcncff  42174  divcncff  42181  cncfiooicclem1  42183  dvsinexp  42202  dvsubf  42205  dvdivf  42214  dvcosax  42218  dvnmul  42235  dvnprodlem1  42238  dvnprodlem2  42239  itgsinexplem1  42246  itgsubsticclem  42267  iblcncfioo  42270  itgiccshift  42272  stoweidlem20  42312  dirkercncflem2  42396  fourierdlem16  42415  fourierdlem21  42420  fourierdlem22  42421  fourierdlem28  42427  fourierdlem39  42438  fourierdlem51  42449  fourierdlem60  42458  fourierdlem61  42459  fourierdlem69  42467  fourierdlem72  42470  fourierdlem73  42471  fourierdlem81  42479  fourierdlem83  42481  fourierdlem84  42482  fourierdlem87  42485  fourierdlem90  42488  fourierdlem93  42491  fourierdlem95  42493  fourierdlem101  42499  fourierdlem103  42501  fourierdlem104  42502  fourierdlem111  42509  etransclem34  42560  etransclem43  42569  etransclem46  42572  sge0tsms  42669  sge0fodjrnlem  42705  sge0iun  42708  sge0isum  42716  sge0seq  42735  meadjun  42751  meadjiunlem  42754  meadjiun  42755  ismeannd  42756  psmeasurelem  42759  omeiunle  42806  ovn02  42857  smfpimioo  43069  smfresal  43070  smfinflem  43098  smflimsuplem3  43103  smfliminflem  43111  aacllem  44909  amgmwlem  44910  amgmlemALT  44911