Theorem feqmptd 6159

Description: Deduction form of dffn5 6151. (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		ffn 5958	. . 3 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴)
3	1, 2	syl 17	. 2 ⊢ (𝜑 → 𝐹 Fn 𝐴)
4		dffn5 6151	. 2 ⊢ (𝐹 Fn 𝐴 ↔ 𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)))
5	3, 4	sylib 207	1 ⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)))

Syntax hints:   → wi 4   = wceq 1475   ↦ cmpt 4643   Fn wfn 5799  ⟶wf 5800  ‘cfv 5804

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pr 4833

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-sbc 3403  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-br 4584  df-opab 4644  df-mpt 4645  df-id 4953  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-fv 5812

This theorem is referenced by:  feqresmpt  6160  fcoconst  6307  ofco  6815  caofinvl  6822  caofcom  6827  caofass  6829  caofdi  6831  caofdir  6832  caonncan  6833  suppssof1  7215  mapxpen  8011  xpmapenlem  8012  cantnfp1  8461  cantnflem1  8469  cnfcom2lem  8481  infxpenc  8724  pwfseqlem5  9364  gruf  9512  ccatco  13432  cnrecnv  13753  lo1o12  14112  rlimclim1  14124  rlimuni  14129  lo1resb  14143  rlimresb  14144  o1resb  14145  rlimcn1  14167  rlimcn1b  14168  rlimo1  14195  o1rlimmul  14197  caucvgr  14254  ackbijnn  14399  bitsf1ocnv  15004  ramcl  15571  pwsplusgval  15973  pwsmulrval  15974  pwsvscafval  15977  setcepi  16561  prf1st  16667  prf2nd  16668  1st2ndprf  16669  curfuncf  16701  curf2ndf  16710  yonedainv  16744  yonffthlem  16745  prdsidlem  17145  pwsco1mhm  17193  pwsco2mhm  17194  frmdup3lem  17226  frmdup3  17227  grpinvcnv  17306  pwsinvg  17351  pwssub  17352  psgnunilem5  17737  efginvrel1  17964  frgpup3lem  18013  frgpup3  18014  gsumval3  18131  gsumcllem  18132  gsumzf1o  18136  gsumzsplit  18150  gsumconst  18157  gsumzmhm  18160  gsumsub  18171  gsum2dlem2  18193  gsumcom2  18197  dprdfadd  18242  dprdfsub  18243  dprdfeq0  18244  dprdf11  18245  dmdprdsplitlem  18259  dprddisj2  18261  dpjidcl  18280  ablfaclem2  18308  ablfac2  18311  mptscmfsuppd  18752  lmhmvsca  18866  rrgsupp  19112  psrbagaddcl  19191  gsumbagdiaglem  19196  psrass1lem  19198  psrlinv  19218  psrass1  19226  psrcom  19230  mplsubrglem  19260  mplmonmul  19285  mplcoe1  19286  mplcoe5  19289  evlslem2  19333  evlslem6  19334  evlslem1  19336  coe1fval3  19399  coe1sclmul  19473  coe1sclmul2  19475  mulgrhm2  19666  cygznlem2a  19735  frgpcyg  19741  uvcresum  19951  frlmup1  19956  grpvrinv  20021  mhmvlin  20022  mdetleib2  20213  mdetralt  20233  mdetunilem9  20245  cayleyhamilton1  20516  neiptopnei  20746  dfac14  21231  ptcnp  21235  lmcn2  21262  cnmpt11f  21277  cnmpt21f  21285  cnmpt2k  21301  qtopeu  21329  xkocnv  21427  xkohmeo  21428  flfcnp2  21621  istgp2  21705  tmdgsum  21709  symgtgp  21715  subgtgp  21719  tgpconcomp  21726  prdstgpd  21738  tsmsmhm  21759  tsmssub  21762  tgptsmscls  21763  tsmssplit  21765  tsmsxplem1  21766  tlmtgp  21809  ustuqtop  21860  prdsmslem1  22142  prdsxmslem1  22143  prdsxmslem2  22144  tngnm  22265  nmoeq0  22350  cnfldnm  22392  cncfmpt1f  22524  negfcncf  22530  cnrehmeo  22560  evth  22566  evth2  22567  copco  22626  pcopt  22630  pcopt2  22631  pcoass  22632  pcorev2  22636  pi1xfrcnv  22665  ovolctb  23065  ovolfs2  23145  uniioombllem2  23157  uniioombllem3  23159  ismbf  23203  mbfconst  23208  ismbfcn2  23212  mbfmulc2re  23221  mbfadd  23234  mbfsub  23235  mbflimsup  23239  itg1climres  23287  mbfi1flimlem  23295  mbfi1flim  23296  mbfmul  23299  itg2uba  23316  itg2mulclem  23319  itg2mulc  23320  itg2splitlem  23321  itg2monolem1  23323  itg2i1fseq  23328  itg2gt0  23333  itg2cnlem1  23334  itg2cnlem2  23335  i1fibl  23380  itgitg1  23381  iblabslem  23400  iblabs  23401  bddmulibl  23411  cnplimc  23457  limccnp  23461  limccnp2  23462  dvcnp2  23489  dvmulf  23512  dvcmulf  23514  dvcobr  23515  dvcof  23517  dvcjbr  23518  dvcj  23519  dvfre  23520  dvmptcj  23537  dvcnvlem  23543  dvcnv  23544  dvef  23547  dvsincos  23548  rolle  23557  cmvth  23558  dvlip  23560  dvlipcn  23561  dv11cn  23568  dvivthlem1  23575  dvivth  23577  lhop2  23582  dvfsumrlim2  23599  ftc1lem1  23602  ftc1lem2  23603  ftc1a  23604  ftc1lem4  23606  ftc2  23611  ftc2ditglem  23612  ftc2ditg  23613  tdeglem4  23624  tdeglem2  23625  mdegle0  23641  mdegmullem  23642  plypf1  23772  plyco  23801  dgrcolem1  23833  dgrcolem2  23834  dgrco  23835  plycjlem  23836  dvply2g  23844  plydiveu  23857  elqaalem3  23880  taylthlem1  23931  taylthlem2  23932  ulmshft  23948  ulmdvlem1  23958  mtest  23962  mtestbdd  23963  mbfulm  23964  iblulm  23965  itgulm  23966  pserulm  23980  pserdv  23987  abelthlem1  23989  abelthlem3  23991  pige3  24073  eff1olem  24098  logcn  24193  advlog  24200  advlogexp  24201  logtayl  24206  logccv  24209  dvcxp1  24281  dvcxp2  24282  dvcncxp1  24284  resqrtcn  24290  sqrtcn  24291  loglesqrt  24299  dvatan  24462  leibpi  24469  divsqrtsumo1  24510  jensenlem2  24514  amgmlem  24516  lgamgulmlem2  24556  lgamcvg2  24581  ftalem7  24605  basellem9  24615  muinv  24719  dchrmulid2  24777  dchrinvcl  24778  lgseisenlem4  24903  dchrisum0lem2a  25006  logdivsum  25022  mulog2sumlem1  25023  log2sumbnd  25033  hilnormi  27404  chscllem4  27883  hmopidmchi  28394  rabfodom  28728  cofmpt  28846  ofoprabco  28847  fpwrelmapffslem  28895  fpwrelmap  28896  qqhre  29392  esumpcvgval  29467  ofcfval4  29494  omssubadd  29689  carsggect  29707  plymulx0  29950  ptpcon  30469  cvmliftlem6  30526  cvmliftlem8  30528  cvmlift2lem7  30545  cvmliftphtlem  30553  cvmlift3lem5  30559  elmsubrn  30679  knoppcnlem9  31661  curunc  32561  poimir  32612  broucube  32613  mblfinlem2  32617  volsupnfl  32624  cnambfre  32628  dvtan  32630  itg2addnclem  32631  itg2addnclem2  32632  itg2addnclem3  32633  itg2addnc  32634  itg2gt0cn  32635  itgaddnc  32640  itgmulc2nc  32648  bddiblnc  32650  ftc1cnnclem  32653  ftc1anclem1  32655  ftc1anclem2  32656  ftc1anclem3  32657  ftc1anclem4  32658  ftc1anclem5  32659  ftc1anclem6  32660  ftc1anclem7  32661  ftc1anclem8  32662  ftc1anc  32663  ftc2nc  32664  upixp  32694  mzpsubst  36329  diophun  36355  mendlmod  36782  mendassa  36783  fsovcnvlem  37327  binomcxplemnotnn0  37577  rnsnf  38365  cncfmptss  38654  mulcncff  38753  subcncff  38765  cncfcompt  38768  addcncff  38770  divcncff  38777  cncfiooicclem1  38779  dvsinexp  38798  dvsubf  38802  dvdivf  38812  dvcosax  38816  dvnmul  38833  dvnprodlem1  38836  dvnprodlem2  38837  itgsinexplem1  38845  itgsubsticclem  38867  iblcncfioo  38870  itgiccshift  38872  stoweidlem20  38913  dirkercncflem2  38997  fourierdlem16  39016  fourierdlem21  39021  fourierdlem22  39022  fourierdlem28  39028  fourierdlem39  39039  fourierdlem51  39050  fourierdlem60  39059  fourierdlem61  39060  fourierdlem69  39068  fourierdlem72  39071  fourierdlem73  39072  fourierdlem81  39080  fourierdlem83  39082  fourierdlem84  39083  fourierdlem87  39086  fourierdlem90  39089  fourierdlem93  39092  fourierdlem95  39094  fourierdlem101  39100  fourierdlem103  39102  fourierdlem104  39103  fourierdlem111  39110  etransclem34  39161  etransclem43  39170  etransclem46  39173  sge0tsms  39273  sge0fodjrnlem  39309  sge0iun  39312  sge0isum  39320  sge0seq  39339  meadjun  39355  meadjiunlem  39358  meadjiun  39359  ismeannd  39360  psmeasurelem  39363  omeiunle  39407  ovn02  39458  smfpimioo  39672  smfresal  39673  aacllem  42356  amgmwlem  42357  amgmlemALT  42358