Theorem feqmptd 5926

Description: Deduction form of dffn5 5918. (Contributed by Mario Carneiro, 8-Jan-2015.)

Hypothesis

Ref	Expression
feqmptd.1

Assertion

Ref	Expression
feqmptd

Distinct variable groups:   ,   ,

Proof of Theorem feqmptd

Step	Hyp	Ref	Expression
1		feqmptd.1	. . 3
2		ffn 5736	. . 3
3	1, 2	syl 16	. 2
4		dffn5 5918	. 2
5	3, 4	sylib 196	1

Syntax hints:  ->wi 4  =wceq 1395  e.cmpt 4510  Fnwfn 5588  -->wf 5589  `cfv 5593

This theorem is referenced by:  feqresmpt  5927  fcoconst  6068  suppssof1OLD  6559  ofco  6560  caofinvl  6567  caofcom  6572  caofass  6574  caofdi  6576  caofdir  6577  caonncan  6578  suppssof1  6952  mapxpen  7703  xpmapenlem  7704  cantnfp1  8121  cantnflem1  8129  cantnfp1OLD  8147  cantnflem1OLD  8152  cnfcom2lem  8166  cnfcom2lemOLD  8174  infxpenc  8416  infxpencOLD  8421  pwfseqlem5  9062  gruf  9210  ccatco  12801  cnrecnv  12998  lo1o12  13356  rlimclim1  13368  rlimuni  13373  lo1resb  13387  rlimresb  13388  o1resb  13389  rlimcn1  13411  rlimcn1b  13412  rlimo1  13439  o1rlimmul  13441  caucvgr  13498  ackbijnn  13640  bitsf1ocnv  14094  ramcl  14547  pwsplusgval  14887  pwsmulrval  14888  pwsvscafval  14891  setcepi  15415  prf1st  15473  prf2nd  15474  1st2ndprf  15475  curfuncf  15507  curf2ndf  15516  yonedainv  15550  yonffthlem  15551  prdsidlem  15952  pwsco1mhm  16001  pwsco2mhm  16002  frmdup3lem  16034  frmdup3  16035  grpinvcnv  16106  pwsinvg  16182  pwssub  16183  psgnunilem5  16519  efginvrel1  16746  frgpup3lem  16795  frgpup3  16796  gsumval3OLD  16908  gsumval3  16911  gsumcllem  16912  gsumcllemOLD  16913  gsumzf1o  16917  gsumzf1oOLD  16920  gsumzsplit  16944  gsumzsplitOLD  16945  gsumconst  16954  gsumzmhm  16957  gsumzmhmOLD  16958  gsumsub  16974  gsumsubOLD  16975  gsum2dlem2  16998  gsum2dOLD  17000  gsumcom2  17003  dprdfadd  17060  dprdfsub  17061  dprdfeq0  17062  dprdf11  17063  dprdfaddOLD  17067  dprdfsubOLD  17068  dprdfeq0OLD  17069  dprdf11OLD  17070  dmdprdsplitlem  17084  dmdprdsplitlemOLD  17085  dprddisj2  17087  dprddisj2OLD  17088  dpjidcl  17107  dpjidclOLD  17114  ablfaclem2  17137  ablfac2  17140  mptscmfsuppd  17577  lmhmvsca  17691  rrgsupp  17939  rrgsuppOLD  17940  psrbagaddcl  18020  psrbagaddclOLD  18021  gsumbagdiaglem  18027  psrass1lem  18029  psrlinv  18050  psrass1  18060  psrcom  18064  mplsubrglem  18100  mplsubrglemOLD  18101  mplmonmul  18126  mplcoe1  18127  mplcoe5  18131  mplcoe2OLD  18133  evlslem2  18180  evlslem6  18181  evlslem6OLD  18182  evlslem1  18184  coe1fval3  18247  coe1sclmul  18323  coe1sclmul2  18325  ply1coeOLD  18338  mulgrhm2  18533  mulgrhm2OLD  18536  cygznlem2a  18606  frgpcyg  18612  uvcresum  18824  frlmup1  18832  grpvrinv  18898  mhmvlin  18899  mdetleib2  19090  mdetralt  19110  mdetunilem9  19122  cayleyhamilton1  19393  neiptopnei  19633  dfac14  20119  ptcnp  20123  lmcn2  20150  cnmpt11f  20165  cnmpt21f  20173  cnmpt2k  20189  qtopeu  20217  xkocnv  20315  xkohmeo  20316  flfcnp2  20508  istgp2  20590  tmdgsum  20594  symgtgp  20600  subgtgp  20604  tgpconcomp  20611  prdstgpd  20623  tsmsmhm  20648  tsmssub  20651  tgptsmscls  20652  tsmssplit  20654  tsmsxplem1  20655  tlmtgp  20698  ustuqtop  20749  prdsmslem1  21030  prdsxmslem1  21031  prdsxmslem2  21032  tngnm  21165  nmoeq0  21243  cnfldnm  21286  cncfmpt1f  21417  negfcncf  21423  cnrehmeo  21453  evth  21459  evth2  21460  copco  21518  pcopt  21522  pcopt2  21523  pcoass  21524  pcorev2  21528  pi1xfrcnv  21557  ovolctb  21901  ovolfs2  21980  uniioombllem2  21992  uniioombllem3  21994  ismbf  22037  mbfconst  22042  ismbfcn2  22046  mbfmulc2re  22055  mbfadd  22068  mbfsub  22069  mbflimsup  22073  itg1climres  22121  mbfi1flimlem  22129  mbfi1flim  22130  mbfmul  22133  itg2uba  22150  itg2mulclem  22153  itg2mulc  22154  itg2splitlem  22155  itg2monolem1  22157  itg2i1fseq  22162  itg2gt0  22167  itg2cnlem1  22168  itg2cnlem2  22169  i1fibl  22214  itgitg1  22215  iblabslem  22234  iblabs  22235  bddmulibl  22245  cnplimc  22291  limccnp  22295  limccnp2  22296  dvcnp2  22323  dvmulf  22346  dvcmulf  22348  dvcobr  22349  dvcof  22351  dvcjbr  22352  dvcj  22353  dvfre  22354  dvmptcj  22371  dvcnvlem  22377  dvcnv  22378  dvef  22381  dvsincos  22382  rolle  22391  cmvth  22392  dvlip  22394  dvlipcn  22395  dv11cn  22402  dvivthlem1  22409  dvivth  22411  lhop2  22416  dvfsumrlim2  22433  ftc1lem1  22436  ftc1lem2  22437  ftc1a  22438  ftc1lem4  22440  ftc2  22445  ftc2ditglem  22446  ftc2ditg  22447  tdeglem4  22458  tdeglem2  22459  mdegle0  22477  mdegmullem  22478  plypf1  22609  plyco  22638  dgrcolem1  22670  dgrcolem2  22671  dgrco  22672  plycjlem  22673  dvply2g  22681  plydiveu  22694  elqaalem3  22717  taylthlem1  22768  taylthlem2  22769  ulmshft  22785  ulmdvlem1  22795  mtest  22799  mtestbdd  22800  mbfulm  22801  iblulm  22802  itgulm  22803  pserulm  22817  pserdv  22824  abelthlem1  22826  abelthlem3  22828  pige3  22910  eff1olem  22935  logcn  23028  advlog  23035  advlogexp  23036  logtayl  23041  logccv  23044  dvcxp1  23116  dvcxp2  23117  resqrtcn  23123  sqrtcn  23124  loglesqrt  23132  dvatan  23266  leibpi  23273  divsqrtsumo1  23313  jensenlem2  23317  amgmlem  23319  ftalem7  23352  basellem9  23362  muinv  23469  dchrmulid2  23527  dchrinvcl  23528  lgseisenlem4  23627  dchrisum0lem2a  23702  logdivsum  23718  mulog2sumlem1  23719  log2sumbnd  23729  hilnormi  26080  chscllem4  26558  hmopidmchi  27070  rabfodom  27404  cofmpt  27504  ofoprabco  27505  fpwrelmapffslem  27555  fpwrelmap  27556  qqhre  27998  esumpcvgval  28084  ofcfval4  28104  plymulx0  28504  lgamgulmlem2  28572  lgamcvg2  28597  ptpcon  28678  cvmliftlem6  28735  cvmliftlem8  28737  cvmlift2lem7  28754  cvmliftphtlem  28762  cvmlift3lem5  28768  elmsubrn  28888  mblfinlem2  30052  volsupnfl  30059  cnambfre  30063  dvtan  30065  itg2addnclem  30066  itg2addnclem2  30067  itg2addnclem3  30068  itg2addnc  30069  itg2gt0cn  30070  itgaddnc  30075  itgmulc2nc  30083  bddiblnc  30085  ftc1cnnclem  30088  ftc1anclem1  30090  ftc1anclem2  30091  ftc1anclem3  30092  ftc1anclem4  30093  ftc1anclem5  30094  ftc1anclem6  30095  ftc1anclem7  30096  ftc1anclem8  30097  ftc1anc  30098  ftc2nc  30099  dvcncxp1  30100  upixp  30220  mzpsubst  30681  diophun  30707  mendlmod  31142  mendassa  31143  binomcxplemnotnn0  31261  cncfmptss  31581  mulcncff  31670  subcncff  31682  cncfcompt  31685  addcncff  31687  divcncff  31694  cncfiooicclem1  31696  dvsinexp  31705  dvsubf  31709  dvdivf  31719  dvcosax  31723  dvnmul  31740  dvnprodlem1  31743  dvnprodlem2  31744  itgsinexplem1  31752  itgsubsticclem  31774  iblcncfioo  31777  itgiccshift  31779  stoweidlem20  31802  dirkercncflem2  31886  fourierdlem16  31905  fourierdlem21  31910  fourierdlem22  31911  fourierdlem28  31917  fourierdlem39  31928  fourierdlem51  31940  fourierdlem60  31949  fourierdlem61  31950  fourierdlem69  31958  fourierdlem72  31961  fourierdlem73  31962  fourierdlem81  31970  fourierdlem83  31972  fourierdlem84  31973  fourierdlem87  31976  fourierdlem90  31979  fourierdlem93  31982  fourierdlem95  31984  fourierdlem101  31990  fourierdlem103  31992  fourierdlem104  31993  fourierdlem111  32000  etransclem34  32051  etransclem43  32060  etransclem46  32063  aacllem  33216

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-9 1822  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-sep 4573  ax-nul 4581  ax-pr 4691

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-eu 2286  df-mo 2287  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3111  df-sbc 3328  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-sn 4030  df-pr 4032  df-op 4036  df-uni 4250  df-br 4453  df-opab 4511  df-mpt 4512  df-id 4800  df-xp 5010  df-rel 5011  df-cnv 5012  df-co 5013  df-dm 5014  df-iota 5556  df-fun 5595  df-fn 5596  df-f 5597  df-fv 5601