Theorem feqmptd 6977

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

Syntax hints:   → wi 4   = wceq 1540   ↦ cmpt 5225   Fn wfn 6556  ⟶wf 6557  ‘cfv 6561

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-opab 5206  df-mpt 5226  df-id 5578  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-fv 6569

This theorem is referenced by:  feqresmpt  6978  cofmpt  7152  fcoconst  7154  ofco  7722  caofinvl  7729  caofcom  7734  caofidlcan  7735  caofass  7737  caofdi  7739  caofdir  7740  caonncan  7741  suppssof1  8224  mapxpen  9183  xpmapenlem  9184  cantnfp1  9721  cantnflem1  9729  cnfcom2lem  9741  infxpenc  10058  pwfseqlem5  10703  gruf  10851  ccatco  14874  cnrecnv  15204  rlimclim1  15581  rlimuni  15586  lo1resb  15600  rlimresb  15601  o1resb  15602  rlimcn1  15624  rlimo1  15653  o1rlimmul  15655  caucvgr  15712  ackbijnn  15864  bitsf1ocnv  16481  ramcl  17067  pwsplusgval  17535  pwsmulrval  17536  pwsvscafval  17539  setcepi  18133  prf1st  18249  prf2nd  18250  1st2ndprf  18251  curfuncf  18283  curf2ndf  18292  yonedainv  18326  yonffthlem  18327  prdsidlem  18782  mhmvlin  18814  pwsco1mhm  18845  pwsco2mhm  18846  frmdup3lem  18879  frmdup3  18880  grpinvcnv  19024  pwsinvg  19071  pwssub  19072  efginvrel1  19746  frgpup3lem  19795  frgpup3  19796  gsumval3  19925  gsumcllem  19926  gsumzf1o  19930  gsumzsplit  19945  gsumconst  19952  gsumzmhm  19955  gsumsub  19966  gsum2dlem2  19989  gsumcom2  19993  dprdfadd  20040  dprdfsub  20041  dprdfeq0  20042  dprdf11  20043  dmdprdsplitlem  20057  dprddisj2  20059  dpjidcl  20078  ablfaclem2  20106  ablfac2  20109  rrgsupp  20701  mptscmfsuppd  20926  lmhmvsca  21044  mulgrhm2  21489  cygznlem2a  21586  frgpcyg  21592  uvcresum  21813  frlmup1  21818  gsumbagdiaglem  21950  psrass1lem  21952  psrlinv  21975  psrass1  21984  psrcom  21988  mplsubrglem  22024  mplmonmul  22054  mplcoe1  22055  mplcoe5  22058  evlslem2  22103  evlslem6  22105  evlslem1  22106  mhpmulcl  22153  psdmplcl  22166  psdmul  22170  coe1fval3  22210  coe1sclmul  22285  coe1sclmul2  22287  grpvrinv  22403  mdetleib2  22594  mdetunilem9  22626  cayleyhamilton1  22898  neiptopnei  23140  dfac14  23626  ptcnp  23630  lmcn2  23657  cnmpt11f  23672  cnmpt21f  23680  cnmpt2k  23696  qtopeu  23724  xkocnv  23822  xkohmeo  23823  flfcnp2  24015  istgp2  24099  tmdgsum  24103  subgtgp  24113  symgtgp  24114  tgpconncomp  24121  prdstgpd  24133  tsmssub  24157  tgptsmscls  24158  tsmssplit  24160  tsmsxplem1  24161  tlmtgp  24204  ustuqtop  24255  prdsmslem1  24540  prdsxmslem1  24541  prdsxmslem2  24542  tngnm  24672  nmoeq0  24757  cnfldnm  24799  cncfmpt1f  24940  negfcncf  24950  cnrehmeo  24984  cnrehmeoOLD  24985  evth  24991  evth2  24992  copco  25051  pcopt  25055  pcopt2  25056  pcoass  25057  pcorev2  25061  pi1xfrcnv  25090  ovolctb  25525  ovolfs2  25606  uniioombllem2  25618  ismbf  25663  mbfconst  25668  mbfmulc2re  25683  mbfadd  25696  mbfsub  25697  mbflimsup  25701  mbfi1flimlem  25757  mbfi1flim  25758  mbfmul  25761  itg2uba  25778  itg2mulclem  25781  itg2mulc  25782  itg2splitlem  25783  itg2monolem1  25785  itg2i1fseq  25790  itg2gt0  25795  itg2cnlem1  25796  itg2cnlem2  25797  i1fibl  25843  itgitg1  25844  bddmulibl  25874  bddiblnc  25877  cnplimc  25922  limccnp2  25927  dvcnp2  25955  dvcnp2OLD  25956  dvmulf  25980  dvcmulf  25982  dvcobr  25983  dvcobrOLD  25984  dvcof  25986  dvcj  25988  dvfre  25989  dvmptcj  26006  dvcnvlem  26014  dvcnv  26015  dvef  26018  dvsincos  26019  rolle  26028  cmvth  26029  cmvthOLD  26030  dvlip  26032  dvlipcn  26033  dv11cn  26040  dvivthlem1  26047  dvivth  26049  lhop2  26054  dvfsumrlim2  26073  ftc1lem1  26076  ftc1lem2  26077  ftc1a  26078  ftc1lem4  26080  ftc2  26085  ftc2ditglem  26086  ftc2ditg  26087  tdeglem4  26099  tdeglem2  26100  mdegle0  26116  mdegmullem  26117  plypf1  26251  plyco  26280  dgrcolem1  26313  dgrcolem2  26314  dgrco  26315  plycjlem  26316  dvply2g  26326  dvply2gOLD  26327  plydiveu  26340  elqaalem3  26363  taylthlem1  26415  taylthlem2  26416  taylthlem2OLD  26417  ulmshft  26433  ulmdvlem1  26443  mtest  26447  mtestbdd  26448  mbfulm  26449  iblulm  26450  itgulm  26451  pserulm  26465  pserdv  26473  abelthlem1  26475  abelthlem3  26477  pige3ALT  26562  eff1olem  26590  logcn  26689  advlog  26696  advlogexp  26697  logtayl  26702  logccv  26705  dvcxp1  26782  dvcxp2  26783  dvcncxp1  26785  resqrtcn  26792  sqrtcn  26793  loglesqrt  26804  dvatan  26978  leibpi  26985  divsqrtsumo1  27027  jensenlem2  27031  amgmlem  27033  lgamgulmlem2  27073  ftalem7  27122  basellem9  27132  muinv  27236  dchrmullid  27296  dchrinvcl  27297  dchrisum0lem2a  27561  logdivsum  27577  mulog2sumlem1  27578  log2sumbnd  27588  hilnormi  31182  chscllem4  31659  hmopidmchi  32170  rabfodom  32524  ofoprabco  32674  fpwrelmapffslem  32743  fpwrelmap  32744  prodindf  32848  gsumwrd2dccat  33070  elrgspn  33250  elrgspnsubrunlem2  33252  lbsdiflsp0  33677  fedgmullem1  33680  qqhre  34021  esumpcvgval  34079  ofcfval4  34106  omssubadd  34302  carsggect  34320  plymulx0  34562  fdvneggt  34615  fdvnegge  34617  itgexpif  34621  ptpconn  35238  cvmliftlem6  35295  cvmliftlem8  35297  cvmlift2lem7  35314  cvmliftphtlem  35322  cvmlift3lem5  35328  elmsubrn  35533  knoppcnlem9  36502  curunc  37609  poimir  37660  broucube  37661  mblfinlem2  37665  volsupnfl  37672  cnambfre  37675  dvtan  37677  itg2addnclem  37678  itg2addnclem2  37679  itg2addnclem3  37680  itg2addnc  37681  itg2gt0cn  37682  itgaddnc  37687  itgmulc2nc  37695  ftc1cnnclem  37698  ftc1anclem1  37700  ftc1anclem2  37701  ftc1anclem3  37702  ftc1anclem4  37703  ftc1anclem5  37704  ftc1anclem6  37705  ftc1anclem7  37706  ftc1anclem8  37707  ftc1anc  37708  ftc2nc  37709  upixp  37736  readvcot  42394  selvvvval  42595  evlselv  42597  fsuppssindlem1  42601  fsuppssindlem2  42602  mhphflem  42606  mhphf  42607  mzpsubst  42759  diophun  42784  mendlmod  43201  mendassa  43202  cantnf2  43338  fsovcnvlem  44026  binomcxplemnotnn0  44375  rnsnf  45189  cncfmptss  45602  climliminflimsupd  45816  mulcncff  45885  subcncff  45895  cncfcompt  45898  addcncff  45899  divcncff  45906  cncfiooicclem1  45908  dvsinexp  45926  dvsubf  45929  dvdivf  45937  dvcosax  45941  dvnmul  45958  dvnprodlem1  45961  dvnprodlem2  45962  itgsinexplem1  45969  itgsubsticclem  45990  iblcncfioo  45993  itgiccshift  45995  stoweidlem20  46035  dirkercncflem2  46119  fourierdlem16  46138  fourierdlem21  46143  fourierdlem22  46144  fourierdlem28  46150  fourierdlem39  46161  fourierdlem51  46172  fourierdlem60  46181  fourierdlem61  46182  fourierdlem69  46190  fourierdlem72  46193  fourierdlem73  46194  fourierdlem81  46202  fourierdlem83  46204  fourierdlem84  46205  fourierdlem87  46208  fourierdlem90  46211  fourierdlem93  46214  fourierdlem95  46216  fourierdlem101  46222  fourierdlem103  46224  fourierdlem104  46225  fourierdlem111  46232  etransclem34  46283  etransclem43  46292  etransclem46  46295  sge0tsms  46395  sge0fodjrnlem  46431  sge0iun  46434  sge0isum  46442  sge0seq  46461  meadjun  46477  meadjiunlem  46480  meadjiun  46481  ismeannd  46482  psmeasurelem  46485  omeiunle  46532  ovn02  46583  smfpimioo  46802  smfresal  46803  smfinflem  46832  smflimsuplem3  46837  smfliminflem  46845  1arymaptfo  48564  diag1  49004  aacllem  49320  amgmwlem  49321  amgmlemALT  49322