Theorem feqmptd 6831

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

Syntax hints:   → wi 4   = wceq 1541   ↦ cmpt 5161   Fn wfn 6425  ⟶wf 6426  ‘cfv 6430

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-10 2140  ax-11 2157  ax-12 2174  ax-ext 2710  ax-sep 5226  ax-nul 5233  ax-pr 5355

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1544  df-fal 1554  df-ex 1786  df-nf 1790  df-sb 2071  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2817  df-nfc 2890  df-ral 3070  df-rex 3071  df-rab 3074  df-v 3432  df-dif 3894  df-un 3896  df-in 3898  df-ss 3908  df-nul 4262  df-if 4465  df-sn 4567  df-pr 4569  df-op 4573  df-uni 4845  df-br 5079  df-opab 5141  df-mpt 5162  df-id 5488  df-xp 5594  df-rel 5595  df-cnv 5596  df-co 5597  df-dm 5598  df-iota 6388  df-fun 6432  df-fn 6433  df-f 6434  df-fv 6438

This theorem is referenced by:  feqresmpt  6832  cofmpt  6998  fcoconst  7000  ofco  7547  caofinvl  7554  caofcom  7559  caofass  7561  caofdi  7563  caofdir  7564  caonncan  7565  suppssof1  7999  mapxpen  8895  xpmapenlem  8896  cantnfp1  9400  cantnflem1  9408  cnfcom2lem  9420  infxpenc  9758  pwfseqlem5  10403  gruf  10551  ccatco  14529  cnrecnv  14857  rlimclim1  15235  rlimuni  15240  lo1resb  15254  rlimresb  15255  o1resb  15256  rlimcn1  15278  rlimo1  15307  o1rlimmul  15309  caucvgr  15368  ackbijnn  15521  bitsf1ocnv  16132  ramcl  16711  pwsplusgval  17182  pwsmulrval  17183  pwsvscafval  17186  setcepi  17784  prf1st  17902  prf2nd  17903  1st2ndprf  17904  curfuncf  17937  curf2ndf  17946  yonedainv  17980  yonffthlem  17981  prdsidlem  18398  pwsco1mhm  18451  pwsco2mhm  18452  frmdup3lem  18486  frmdup3  18487  grpinvcnv  18624  pwsinvg  18669  pwssub  18670  efginvrel1  19315  frgpup3lem  19364  frgpup3  19365  gsumval3  19489  gsumcllem  19490  gsumzf1o  19494  gsumzsplit  19509  gsumconst  19516  gsumzmhm  19519  gsumsub  19530  gsum2dlem2  19553  gsumcom2  19557  dprdfadd  19604  dprdfsub  19605  dprdfeq0  19606  dprdf11  19607  dmdprdsplitlem  19621  dprddisj2  19623  dpjidcl  19642  ablfaclem2  19670  ablfac2  19673  mptscmfsuppd  20170  lmhmvsca  20288  rrgsupp  20543  mulgrhm2  20681  cygznlem2a  20756  frgpcyg  20762  uvcresum  20981  frlmup1  20986  psrbagaddclOLD  21113  gsumbagdiaglemOLD  21122  psrass1lemOLD  21124  gsumbagdiaglem  21125  psrass1lem  21127  psrlinv  21147  psrass1  21155  psrcom  21159  mplsubrglem  21191  mplmonmul  21218  mplcoe1  21219  mplcoe5  21222  evlslem2  21270  evlslem6  21272  evlslem1  21273  mhpmulcl  21320  coe1fval3  21360  coe1sclmul  21434  coe1sclmul2  21436  grpvrinv  21526  mhmvlin  21527  mdetleib2  21718  mdetunilem9  21750  cayleyhamilton1  22022  neiptopnei  22264  dfac14  22750  ptcnp  22754  lmcn2  22781  cnmpt11f  22796  cnmpt21f  22804  cnmpt2k  22820  qtopeu  22848  xkocnv  22946  xkohmeo  22947  flfcnp2  23139  istgp2  23223  tmdgsum  23227  subgtgp  23237  symgtgp  23238  tgpconncomp  23245  prdstgpd  23257  tsmssub  23281  tgptsmscls  23282  tsmssplit  23284  tsmsxplem1  23285  tlmtgp  23328  ustuqtop  23379  prdsmslem1  23664  prdsxmslem1  23665  prdsxmslem2  23666  tngnm  23796  nmoeq0  23881  cnfldnm  23923  cncfmpt1f  24058  negfcncf  24067  cnrehmeo  24097  evth  24103  evth2  24104  copco  24162  pcopt  24166  pcopt2  24167  pcoass  24168  pcorev2  24172  pi1xfrcnv  24201  ovolctb  24635  ovolfs2  24716  uniioombllem2  24728  ismbf  24773  mbfconst  24778  mbfmulc2re  24793  mbfadd  24806  mbfsub  24807  mbflimsup  24811  mbfi1flimlem  24868  mbfi1flim  24869  mbfmul  24872  itg2uba  24889  itg2mulclem  24892  itg2mulc  24893  itg2splitlem  24894  itg2monolem1  24896  itg2i1fseq  24901  itg2gt0  24906  itg2cnlem1  24907  itg2cnlem2  24908  i1fibl  24953  itgitg1  24954  bddmulibl  24984  bddiblnc  24987  cnplimc  25032  limccnp2  25037  dvcnp2  25065  dvmulf  25088  dvcmulf  25090  dvcobr  25091  dvcof  25093  dvcj  25095  dvfre  25096  dvmptcj  25113  dvcnvlem  25121  dvcnv  25122  dvef  25125  dvsincos  25126  rolle  25135  cmvth  25136  dvlip  25138  dvlipcn  25139  dv11cn  25146  dvivthlem1  25153  dvivth  25155  lhop2  25160  dvfsumrlim2  25177  ftc1lem1  25180  ftc1lem2  25181  ftc1a  25182  ftc1lem4  25184  ftc2  25189  ftc2ditglem  25190  ftc2ditg  25191  tdeglem4  25205  tdeglem4OLD  25206  tdeglem2  25207  mdegle0  25223  mdegmullem  25224  plypf1  25354  plyco  25383  dgrcolem1  25415  dgrcolem2  25416  dgrco  25417  plycjlem  25418  dvply2g  25426  plydiveu  25439  elqaalem3  25462  taylthlem1  25513  taylthlem2  25514  ulmshft  25530  ulmdvlem1  25540  mtest  25544  mtestbdd  25545  mbfulm  25546  iblulm  25547  itgulm  25548  pserulm  25562  pserdv  25569  abelthlem1  25571  abelthlem3  25573  pige3ALT  25657  eff1olem  25685  logcn  25783  advlog  25790  advlogexp  25791  logtayl  25796  logccv  25799  dvcxp1  25874  dvcxp2  25875  dvcncxp1  25877  resqrtcn  25883  sqrtcn  25884  loglesqrt  25892  dvatan  26066  leibpi  26073  divsqrtsumo1  26114  jensenlem2  26118  amgmlem  26120  lgamgulmlem2  26160  ftalem7  26209  basellem9  26219  muinv  26323  dchrmulid2  26381  dchrinvcl  26382  dchrisum0lem2a  26646  logdivsum  26662  mulog2sumlem1  26663  log2sumbnd  26673  hilnormi  29504  chscllem4  29981  hmopidmchi  30492  rabfodom  30830  ofoprabco  30980  fpwrelmapffslem  31046  fpwrelmap  31047  lbsdiflsp0  31686  fedgmullem1  31689  qqhre  31949  prodindf  31970  esumpcvgval  32025  ofcfval4  32052  omssubadd  32246  carsggect  32264  plymulx0  32505  fdvneggt  32559  fdvnegge  32561  itgexpif  32565  ptpconn  33174  cvmliftlem6  33231  cvmliftlem8  33233  cvmlift2lem7  33250  cvmliftphtlem  33258  cvmlift3lem5  33264  elmsubrn  33469  knoppcnlem9  34660  curunc  35738  poimir  35789  broucube  35790  mblfinlem2  35794  volsupnfl  35801  cnambfre  35804  dvtan  35806  itg2addnclem  35807  itg2addnclem2  35808  itg2addnclem3  35809  itg2addnc  35810  itg2gt0cn  35811  itgaddnc  35816  itgmulc2nc  35824  ftc1cnnclem  35827  ftc1anclem1  35829  ftc1anclem2  35830  ftc1anclem3  35831  ftc1anclem4  35832  ftc1anclem5  35833  ftc1anclem6  35834  ftc1anclem7  35835  ftc1anclem8  35836  ftc1anc  35837  ftc2nc  35838  upixp  35866  fsuppssindlem1  40260  fsuppssindlem2  40261  mhphflem  40264  mhphf  40265  mzpsubst  40550  diophun  40575  mendlmod  40998  mendassa  40999  fsovcnvlem  41574  binomcxplemnotnn0  41927  rnsnf  42674  cncfmptss  43082  climliminflimsupd  43296  mulcncff  43365  subcncff  43375  cncfcompt  43378  addcncff  43379  divcncff  43386  cncfiooicclem1  43388  dvsinexp  43406  dvsubf  43409  dvdivf  43417  dvcosax  43421  dvnmul  43438  dvnprodlem1  43441  dvnprodlem2  43442  itgsinexplem1  43449  itgsubsticclem  43470  iblcncfioo  43473  itgiccshift  43475  stoweidlem20  43515  dirkercncflem2  43599  fourierdlem16  43618  fourierdlem21  43623  fourierdlem22  43624  fourierdlem28  43630  fourierdlem39  43641  fourierdlem51  43652  fourierdlem60  43661  fourierdlem61  43662  fourierdlem69  43670  fourierdlem72  43673  fourierdlem73  43674  fourierdlem81  43682  fourierdlem83  43684  fourierdlem84  43685  fourierdlem87  43688  fourierdlem90  43691  fourierdlem93  43694  fourierdlem95  43696  fourierdlem101  43702  fourierdlem103  43704  fourierdlem104  43705  fourierdlem111  43712  etransclem34  43763  etransclem43  43772  etransclem46  43775  sge0tsms  43872  sge0fodjrnlem  43908  sge0iun  43911  sge0isum  43919  sge0seq  43938  meadjun  43954  meadjiunlem  43957  meadjiun  43958  ismeannd  43959  psmeasurelem  43962  omeiunle  44009  ovn02  44060  smfpimioo  44272  smfresal  44273  smfinflem  44301  smflimsuplem3  44306  smfliminflem  44314  1arymaptfo  45941  aacllem  46457  amgmwlem  46458  amgmlemALT  46459