Theorem feqmptd 6561

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

Syntax hints:   → wi 4   = wceq 1508   ↦ cmpt 5005   Fn wfn 6181  ⟶wf 6182  ‘cfv 6186

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1759  ax-4 1773  ax-5 1870  ax-6 1929  ax-7 1966  ax-8 2053  ax-9 2060  ax-10 2080  ax-11 2094  ax-12 2107  ax-13 2302  ax-ext 2745  ax-sep 5057  ax-nul 5064  ax-pr 5183

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 835  df-3an 1071  df-tru 1511  df-ex 1744  df-nf 1748  df-sb 2017  df-mo 2548  df-eu 2585  df-clab 2754  df-cleq 2766  df-clel 2841  df-nfc 2913  df-ral 3088  df-rex 3089  df-rab 3092  df-v 3412  df-sbc 3677  df-dif 3827  df-un 3829  df-in 3831  df-ss 3838  df-nul 4174  df-if 4346  df-sn 4437  df-pr 4439  df-op 4443  df-uni 4710  df-br 4927  df-opab 4989  df-mpt 5006  df-id 5309  df-xp 5410  df-rel 5411  df-cnv 5412  df-co 5413  df-dm 5414  df-iota 6150  df-fun 6188  df-fn 6189  df-f 6190  df-fv 6194

This theorem is referenced by:  feqresmpt  6562  cofmpt  6716  fcoconst  6718  ofco  7246  caofinvl  7253  caofcom  7258  caofass  7260  caofdi  7262  caofdir  7263  caonncan  7264  suppssof1  7665  mapxpen  8478  xpmapenlem  8479  cantnfp1  8937  cantnflem1  8945  cnfcom2lem  8957  infxpenc  9237  pwfseqlem5  9882  gruf  10030  ccatco  14058  cnrecnv  14384  rlimclim1  14762  rlimuni  14767  lo1resb  14781  rlimresb  14782  o1resb  14783  rlimcn1  14805  rlimo1  14833  o1rlimmul  14835  caucvgr  14892  ackbijnn  15042  bitsf1ocnv  15652  ramcl  16220  pwsplusgval  16618  pwsmulrval  16619  pwsvscafval  16622  setcepi  17219  prf1st  17325  prf2nd  17326  1st2ndprf  17327  curfuncf  17359  curf2ndf  17368  yonedainv  17402  yonffthlem  17403  prdsidlem  17803  pwsco1mhm  17851  pwsco2mhm  17852  frmdup3lem  17885  frmdup3  17886  grpinvcnv  17967  pwsinvg  18012  pwssub  18013  psgnunilem5OLD  18397  efginvrel1  18625  frgpup3lem  18676  frgpup3  18677  gsumval3  18794  gsumcllem  18795  gsumzf1o  18799  gsumzsplit  18813  gsumconst  18820  gsumzmhm  18823  gsumsub  18834  gsum2dlem2  18857  gsumcom2  18861  dprdfadd  18905  dprdfsub  18906  dprdfeq0  18907  dprdf11  18908  dmdprdsplitlem  18922  dprddisj2  18924  dpjidcl  18943  ablfaclem2  18971  ablfac2  18974  mptscmfsuppd  19435  lmhmvsca  19552  rrgsupp  19798  psrbagaddcl  19877  gsumbagdiaglem  19882  psrass1lem  19884  psrlinv  19904  psrass1  19912  psrcom  19916  mplsubrglem  19946  mplmonmul  19971  mplcoe1  19972  mplcoe5  19975  evlslem2  20018  evlslem6  20019  evlslem1  20021  coe1fval3  20095  coe1sclmul  20169  coe1sclmul2  20171  mulgrhm2  20364  cygznlem2a  20432  frgpcyg  20438  uvcresum  20655  frlmup1  20660  grpvrinv  20725  mhmvlin  20726  mdetleib2  20917  mdetunilem9  20949  cayleyhamilton1  21220  neiptopnei  21460  dfac14  21946  ptcnp  21950  lmcn2  21977  cnmpt11f  21992  cnmpt21f  22000  cnmpt2k  22016  qtopeu  22044  xkocnv  22142  xkohmeo  22143  flfcnp2  22335  istgp2  22419  tmdgsum  22423  symgtgp  22429  subgtgp  22433  tgpconncomp  22440  prdstgpd  22452  tsmssub  22476  tgptsmscls  22477  tsmssplit  22479  tsmsxplem1  22480  tlmtgp  22523  ustuqtop  22574  prdsmslem1  22856  prdsxmslem1  22857  prdsxmslem2  22858  tngnm  22979  nmoeq0  23064  cnfldnm  23106  cncfmpt1f  23240  negfcncf  23246  cnrehmeo  23276  evth  23282  evth2  23283  copco  23341  pcopt  23345  pcopt2  23346  pcoass  23347  pcorev2  23351  pi1xfrcnv  23380  ovolctb  23810  ovolfs2  23891  uniioombllem2  23903  ismbf  23948  mbfconst  23953  mbfmulc2re  23968  mbfadd  23981  mbfsub  23982  mbflimsup  23986  mbfi1flimlem  24042  mbfi1flim  24043  mbfmul  24046  itg2uba  24063  itg2mulclem  24066  itg2mulc  24067  itg2splitlem  24068  itg2monolem1  24070  itg2i1fseq  24075  itg2gt0  24080  itg2cnlem1  24081  itg2cnlem2  24082  i1fibl  24127  itgitg1  24128  bddmulibl  24158  cnplimc  24204  limccnp2  24209  dvcnp2  24236  dvmulf  24259  dvcmulf  24261  dvcobr  24262  dvcof  24264  dvcj  24266  dvfre  24267  dvmptcj  24284  dvcnvlem  24292  dvcnv  24293  dvef  24296  dvsincos  24297  rolle  24306  cmvth  24307  dvlip  24309  dvlipcn  24310  dv11cn  24317  dvivthlem1  24324  dvivth  24326  lhop2  24331  dvfsumrlim2  24348  ftc1lem1  24351  ftc1lem2  24352  ftc1a  24353  ftc1lem4  24355  ftc2  24360  ftc2ditglem  24361  ftc2ditg  24362  tdeglem4  24373  tdeglem2  24374  mdegle0  24390  mdegmullem  24391  plypf1  24521  plyco  24550  dgrcolem1  24582  dgrcolem2  24583  dgrco  24584  plycjlem  24585  dvply2g  24593  plydiveu  24606  elqaalem3  24629  taylthlem1  24680  taylthlem2  24681  ulmshft  24697  ulmdvlem1  24707  mtest  24711  mtestbdd  24712  mbfulm  24713  iblulm  24714  itgulm  24715  pserulm  24729  pserdv  24736  abelthlem1  24738  abelthlem3  24740  pige3ALT  24824  eff1olem  24849  logcn  24947  advlog  24954  advlogexp  24955  logtayl  24960  logccv  24963  dvcxp1  25038  dvcxp2  25039  dvcncxp1  25041  resqrtcn  25047  sqrtcn  25048  loglesqrt  25056  dvatan  25230  leibpi  25238  divsqrtsumo1  25279  jensenlem2  25283  amgmlem  25285  lgamgulmlem2  25325  ftalem7  25374  basellem9  25384  muinv  25488  dchrmulid2  25546  dchrinvcl  25547  dchrisum0lem2a  25811  logdivsum  25827  mulog2sumlem1  25828  log2sumbnd  25838  hilnormi  28735  chscllem4  29214  hmopidmchi  29725  rabfodom  30061  ofoprabco  30189  fpwrelmapffslem  30245  fpwrelmap  30246  lbsdiflsp0  30684  fedgmullem1  30687  qqhre  30938  prodindf  30959  esumpcvgval  31014  ofcfval4  31041  omssubadd  31236  carsggect  31254  plymulx0  31496  fdvneggt  31552  fdvnegge  31554  itgexpif  31558  ptpconn  32098  cvmliftlem6  32155  cvmliftlem8  32157  cvmlift2lem7  32174  cvmliftphtlem  32182  cvmlift3lem5  32188  elmsubrn  32328  knoppcnlem9  33393  curunc  34348  poimir  34399  broucube  34400  mblfinlem2  34404  volsupnfl  34411  cnambfre  34414  dvtan  34416  itg2addnclem  34417  itg2addnclem2  34418  itg2addnclem3  34419  itg2addnc  34420  itg2gt0cn  34421  itgaddnc  34426  itgmulc2nc  34434  bddiblnc  34436  ftc1cnnclem  34439  ftc1anclem1  34441  ftc1anclem2  34442  ftc1anclem3  34443  ftc1anclem4  34444  ftc1anclem5  34445  ftc1anclem6  34446  ftc1anclem7  34447  ftc1anclem8  34448  ftc1anc  34449  ftc2nc  34450  upixp  34479  mzpsubst  38774  diophun  38800  mendlmod  39223  mendassa  39224  fsovcnvlem  39756  binomcxplemnotnn0  40138  rnsnf  40899  cncfmptss  41329  climliminflimsupd  41543  mulcncff  41611  subcncff  41623  cncfcompt  41626  addcncff  41627  divcncff  41634  cncfiooicclem1  41636  dvsinexp  41655  dvsubf  41658  dvdivf  41667  dvcosax  41671  dvnmul  41688  dvnprodlem1  41691  dvnprodlem2  41692  itgsinexplem1  41699  itgsubsticclem  41720  iblcncfioo  41723  itgiccshift  41725  stoweidlem20  41766  dirkercncflem2  41850  fourierdlem16  41869  fourierdlem21  41874  fourierdlem22  41875  fourierdlem28  41881  fourierdlem39  41892  fourierdlem51  41903  fourierdlem60  41912  fourierdlem61  41913  fourierdlem69  41921  fourierdlem72  41924  fourierdlem73  41925  fourierdlem81  41933  fourierdlem83  41935  fourierdlem84  41936  fourierdlem87  41939  fourierdlem90  41942  fourierdlem93  41945  fourierdlem95  41947  fourierdlem101  41953  fourierdlem103  41955  fourierdlem104  41956  fourierdlem111  41963  etransclem34  42014  etransclem43  42023  etransclem46  42026  sge0tsms  42123  sge0fodjrnlem  42159  sge0iun  42162  sge0isum  42170  sge0seq  42189  meadjun  42205  meadjiunlem  42208  meadjiun  42209  ismeannd  42210  psmeasurelem  42213  omeiunle  42260  ovn02  42311  smfpimioo  42523  smfresal  42524  smfinflem  42552  smflimsuplem3  42557  smfliminflem  42565  aacllem  44299  amgmwlem  44300  amgmlemALT  44301