Theorem feqmptd 6958

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569   ↦ cmpt 5185   Fn wfn 6538  ⟶wf 6539  ‘cfv 6543

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pr 5391

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3897  df-dif 4046  df-in 4090  df-un 4150  df-nul 4278  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-opab 5167  df-mpt 5186  df-id 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-iota 6497  df-fun 6545  df-fn 6546  df-f 6547  df-fv 6551

This theorem is used by:  feqresmpt  6959  cofmpt  7138  fcoconst  7140  ofco  7722  caofinvl  7729  caofcom  7734  caofidlcan  7735  caofass  7737  caofdi  7739  caofdir  7740  caonncan  7741  suppssof1  8223  mapxpen  9169  xpmapenlem  9170  cantnfp1  9689  cantnflem1  9697  cnfcom2lem  9709  infxpenc  10104  pwfseqlem5  10755  gruf  10903  ccatco  14994  cnrecnv  15341  rlimclim1  15721  rlimuni  15726  lo1resb  15740  rlimresb  15741  o1resb  15742  rlimcn1  15764  rlimo1  15793  o1rlimmul  15795  caucvgr  15852  ackbijnn  16006  bitsf1ocnv  16623  ramcl  17216  pwsplusgval  17671  pwsmulrval  17672  pwsvscafval  17675  setcepi  18272  prf1st  18387  prf2nd  18388  1st2ndprf  18389  curfuncf  18421  curf2ndf  18430  yonedainv  18464  yonffthlem  18465  prdsidlem  18972  mhmvlin  19005  pwsco1mhm  19037  pwsco2mhm  19038  frmdup3lem  19071  frmdup3  19072  grpinvcnv  19226  pwsinvg  19272  pwssub  19273  efginvrel1  19951  frgpup3lem  20000  frgpup3  20001  gsumval3  20130  gsumcllem  20131  gsumzf1o  20135  gsumzsplit  20150  gsumconst  20157  gsumzmhm  20160  gsumsub  20171  gsum2dlem2  20194  gsumcom2  20198  dprdfadd  20245  dprdfsub  20246  dprdfeq0  20247  dprdf11  20248  dmdprdsplitlem  20262  dprddisj2  20264  dpjidcl  20283  ablfaclem2  20311  ablfac2  20314  rrgsupp  20962  mptscmfsuppd  21212  lmhmvsca  21329  mulgrhm2  21793  cygznlem2a  21882  frgpcyg  21888  uvcresum  22108  frlmup1  22113  gsumbagdiaglem  22248  psrass1lem  22250  psrlinv  22272  psrass1  22280  psrcom  22284  mplsubrglem  22320  mplmonmul  22354  mplcoe1  22355  mplcoe5  22358  evlslem2  22397  evlslem6  22399  evlslem1  22400  selvvvval  22460  mhpmulcl  22479  psdmplcl  22492  psdmul  22496  coe1fval3  22535  coe1sclmul  22610  coe1sclmul2  22612  grpvrinv  22723  mdetleib2  22912  mdetunilem9  22944  cayleyhamilton1  23219  neiptopnei  23459  dfac14  23946  ptcnp  23950  lmcn2  23977  cnmpt11f  23992  cnmpt21f  24000  cnmpt2k  24016  qtopeu  24044  xkocnv  24142  xkohmeo  24143  flfcnp2  24335  istgp2  24419  tmdgsum  24423  subgtgp  24433  symgtgp  24434  tgpconncomp  24441  prdstgpd  24453  tsmssub  24477  tgptsmscls  24478  tsmssplit  24480  tsmsxplem1  24481  tlmtgp  24524  ustuqtop  24574  prdsmslem1  24855  prdsxmslem1  24856  prdsxmslem2  24857  tngnm  24979  nmoeq0  25064  cnfldnm  25106  cncfmpt1f  25244  negfcncf  25253  cnrehmeo  25283  evth  25289  evth2  25290  copco  25348  pcopt  25352  pcopt2  25353  pcoass  25354  pcorev2  25358  pi1xfrcnv  25387  ovolctb  25820  ovolfs2  25901  uniioombllem2  25913  ismbf  25958  mbfconst  25963  mbfmulc2re  25978  mbfadd  25991  mbfsub  25992  mbflimsup  25996  mbfi1flimlem  26052  mbfi1flim  26053  mbfmul  26056  itg2uba  26073  itg2mulclem  26076  itg2mulc  26077  itg2splitlem  26078  itg2monolem1  26080  itg2i1fseq  26085  itg2gt0  26090  itg2cnlem1  26091  itg2cnlem2  26092  i1fibl  26137  itgitg1  26138  bddmulibl  26168  bddiblnc  26171  cnplimc  26216  limccnp2  26221  dvcnp2  26249  dvmulf  26272  dvcmulf  26274  dvcobr  26275  dvcof  26277  dvcj  26279  dvfre  26280  dvmptcj  26297  dvcnvlem  26305  dvcnv  26306  dvef  26309  dvsincos  26310  rolle  26319  cmvth  26320  dvlip  26322  dvlipcn  26323  dv11cn  26330  dvivthlem1  26337  dvivth  26339  lhop2  26344  dvfsumrlim2  26361  ftc1lem1  26364  ftc1lem2  26365  ftc1a  26366  ftc1lem4  26368  ftc2  26373  ftc2ditglem  26374  ftc2ditg  26375  tdeglem4  26387  tdeglem2  26388  mdegle0  26404  mdegmullem  26405  plypf1  26540  plyco  26569  dgrcolem1  26601  dgrcolem2  26602  dgrco  26603  plycjlem  26604  plyn0mulidp  26611  dvply2g  26615  plydiveu  26628  elqaalem3  26653  taylthlem1  26709  taylthlem2  26710  ulmshft  26726  ulmdvlem1  26736  mtest  26740  mtestbdd  26741  mbfulm  26742  iblulm  26743  itgulm  26744  pserulm  26758  pserdv  26765  abelthlem1  26767  abelthlem3  26769  pige3ALT  26857  eff1olem  26885  logcn  26984  advlog  26991  advlogexp  26992  logtayl  26997  logccv  27000  dvcxp1  27077  dvcxp2  27078  dvcncxp1  27080  resqrtcn  27086  sqrtcn  27087  loglesqrt  27098  dvatan  27272  leibpi  27279  divsqrtsumo1  27320  jensenlem2  27324  amgmlem  27326  lgamgulmlem2  27366  ftalem7  27415  basellem9  27425  muinv  27529  dchrmullid  27588  dchrinvcl  27589  dchrisum0lem2a  27853  logdivsum  27869  mulog2sumlem1  27870  log2sumbnd  27880  hilnormi  31774  chscllem4  32251  hmopidmchi  32762  rabfodom  33152  ofoprabco  33309  fpwrelmapffslem  33374  fpwrelmap  33375  prodindf  33479  gsummulsubdishift1  33679  gsumwrd2dccat  33689  elrgspn  33857  elrgspnsubrunlem2  33859  domnprodeq0  33890  deg1prod  34165  selvply1rhmlem2  34203  selvply1rhmlem4  34205  selvply1rhm0  34208  mplmulmvr  34221  evlextv  34224  mplvrpmfgalem  34226  mplvrpmga  34227  mplvrpmrhm  34229  psrgsum  34230  psrmonmul  34232  psrmonprod  34234  issply  34243  esplyfval0  34246  esplyfvaln  34256  lbsdiflsp0  34308  fedgmullem1  34311  extdgfialglem2  34375  qqhre  34702  esumpcvgval  34760  ofcfval4  34787  omssubadd  34982  carsggect  35000  fdvneggt  35279  fdvnegge  35281  itgexpif  35285  ptpconn  36088  cvmliftlem6  36145  cvmliftlem8  36147  cvmlift2lem7  36164  cvmliftphtlem  36172  cvmlift3lem5  36178  elmsubrn  36383  knoppcnlem9  37463  curunc  38634  poimir  38680  broucube  38681  mblfinlem2  38685  volsupnfl  38692  cnambfre  38695  dvtan  38697  itg2addnclem  38698  itg2addnclem2  38699  itg2addnclem3  38700  itg2addnc  38701  itg2gt0cn  38702  itgaddnc  38707  itgmulc2nc  38715  ftc1cnnclem  38718  ftc1anclem1  38720  ftc1anclem2  38721  ftc1anclem3  38722  ftc1anclem4  38723  ftc1anclem5  38724  ftc1anclem6  38725  ftc1anclem7  38726  ftc1anclem8  38727  ftc1anc  38728  ftc2nc  38729  upixp  38772  readvcot  43524  evlselv  43726  fsuppssindlem1  43728  fsuppssindlem2  43729  mhphflem  43733  mhphf  43734  mzpsubst  43868  diophun  43893  mendlmod  44300  mendassa  44301  cantnf2  44436  fsovcnvlem  45122  binomcxplemnotnn0  45449  rnsnf  46307  cncfmptss  46707  climliminflimsupd  46919  mulcncff  46988  subcncff  46998  cncfcompt  47001  addcncff  47002  divcncff  47009  cncfiooicclem1  47011  dvsinexp  47029  dvsubf  47032  dvdivf  47040  dvcosax  47044  dvnmul  47061  dvnprodlem1  47064  dvnprodlem2  47065  itgsinexplem1  47072  itgsubsticclem  47093  iblcncfioo  47096  itgiccshift  47098  stoweidlem20  47138  dirkercncflem2  47222  fourierdlem16  47241  fourierdlem21  47246  fourierdlem22  47247  fourierdlem28  47253  fourierdlem39  47264  fourierdlem51  47275  fourierdlem60  47284  fourierdlem61  47285  fourierdlem69  47293  fourierdlem72  47296  fourierdlem73  47297  fourierdlem81  47305  fourierdlem83  47307  fourierdlem84  47308  fourierdlem87  47311  fourierdlem90  47314  fourierdlem93  47317  fourierdlem95  47319  fourierdlem101  47325  fourierdlem103  47327  fourierdlem104  47328  fourierdlem111  47335  etransclem34  47386  etransclem43  47395  etransclem46  47398  sge0tsms  47498  sge0fodjrnlem  47534  sge0iun  47537  sge0isum  47545  sge0seq  47564  meadjun  47580  meadjiunlem  47583  meadjiun  47584  ismeannd  47585  psmeasurelem  47588  omeiunle  47635  ovn02  47686  smfpimioo  47905  smfresal  47906  smfinflem  47935  smflimsuplem3  47940  smfliminflem  47948  1arymaptfo  49863  diag1  50534  dvsec  51039  dvcsc  51040  dvcot  51041  aacllem  51122  amgmwlem  51170  amgmlemALT  51171