MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  feqmptd Structured version   Visualization version   GIF version

Theorem feqmptd 6288
Description: Deduction form of dffn5 6280. (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
StepHypRef Expression
1 feqmptd.1 . . 3 (𝜑𝐹:𝐴𝐵)
2 ffn 6083 . . 3 (𝐹:𝐴𝐵𝐹 Fn 𝐴)
31, 2syl 17 . 2 (𝜑𝐹 Fn 𝐴)
4 dffn5 6280 . 2 (𝐹 Fn 𝐴𝐹 = (𝑥𝐴 ↦ (𝐹𝑥)))
53, 4sylib 208 1 (𝜑𝐹 = (𝑥𝐴 ↦ (𝐹𝑥)))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1523  cmpt 4762   Fn wfn 5921  wf 5922  cfv 5926
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-nul 4822  ax-pr 4936
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ral 2946  df-rex 2947  df-rab 2950  df-v 3233  df-sbc 3469  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-sn 4211  df-pr 4213  df-op 4217  df-uni 4469  df-br 4686  df-opab 4746  df-mpt 4763  df-id 5053  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-fv 5934
This theorem is referenced by:  feqresmpt  6289  cofmpt  6439  fcoconst  6441  ofco  6959  caofinvl  6966  caofcom  6971  caofass  6973  caofdi  6975  caofdir  6976  caonncan  6977  suppssof1  7373  mapxpen  8167  xpmapenlem  8168  cantnfp1  8616  cantnflem1  8624  cnfcom2lem  8636  infxpenc  8879  pwfseqlem5  9523  gruf  9671  ccatco  13627  cnrecnv  13949  lo1o12  14308  rlimclim1  14320  rlimuni  14325  lo1resb  14339  rlimresb  14340  o1resb  14341  rlimcn1  14363  rlimcn1b  14364  rlimo1  14391  o1rlimmul  14393  caucvgr  14450  ackbijnn  14604  bitsf1ocnv  15213  ramcl  15780  pwsplusgval  16197  pwsmulrval  16198  pwsvscafval  16201  setcepi  16785  prf1st  16891  prf2nd  16892  1st2ndprf  16893  curfuncf  16925  curf2ndf  16934  yonedainv  16968  yonffthlem  16969  prdsidlem  17369  pwsco1mhm  17417  pwsco2mhm  17418  frmdup3lem  17450  frmdup3  17451  grpinvcnv  17530  pwsinvg  17575  pwssub  17576  psgnunilem5  17960  efginvrel1  18187  frgpup3lem  18236  frgpup3  18237  gsumval3  18354  gsumcllem  18355  gsumzf1o  18359  gsumzsplit  18373  gsumconst  18380  gsumzmhm  18383  gsumsub  18394  gsum2dlem2  18416  gsumcom2  18420  dprdfadd  18465  dprdfsub  18466  dprdfeq0  18467  dprdf11  18468  dmdprdsplitlem  18482  dprddisj2  18484  dpjidcl  18503  ablfaclem2  18531  ablfac2  18534  mptscmfsuppd  18977  lmhmvsca  19093  rrgsupp  19339  psrbagaddcl  19418  gsumbagdiaglem  19423  psrass1lem  19425  psrlinv  19445  psrass1  19453  psrcom  19457  mplsubrglem  19487  mplmonmul  19512  mplcoe1  19513  mplcoe5  19516  evlslem2  19560  evlslem6  19561  evlslem1  19563  coe1fval3  19626  coe1sclmul  19700  coe1sclmul2  19702  mulgrhm2  19895  cygznlem2a  19964  frgpcyg  19970  uvcresum  20180  frlmup1  20185  grpvrinv  20250  mhmvlin  20251  mdetleib2  20442  mdetralt  20462  mdetunilem9  20474  cayleyhamilton1  20745  neiptopnei  20984  dfac14  21469  ptcnp  21473  lmcn2  21500  cnmpt11f  21515  cnmpt21f  21523  cnmpt2k  21539  qtopeu  21567  xkocnv  21665  xkohmeo  21666  flfcnp2  21858  istgp2  21942  tmdgsum  21946  symgtgp  21952  subgtgp  21956  tgpconncomp  21963  prdstgpd  21975  tsmsmhm  21996  tsmssub  21999  tgptsmscls  22000  tsmssplit  22002  tsmsxplem1  22003  tlmtgp  22046  ustuqtop  22097  prdsmslem1  22379  prdsxmslem1  22380  prdsxmslem2  22381  tngnm  22502  nmoeq0  22587  cnfldnm  22629  cncfmpt1f  22763  negfcncf  22769  cnrehmeo  22799  evth  22805  evth2  22806  copco  22864  pcopt  22868  pcopt2  22869  pcoass  22870  pcorev2  22874  pi1xfrcnv  22903  ovolctb  23304  ovolfs2  23385  uniioombllem2  23397  uniioombllem3  23399  ismbf  23442  mbfconst  23447  ismbfcn2  23451  mbfmulc2re  23460  mbfadd  23473  mbfsub  23474  mbflimsup  23478  itg1climres  23526  mbfi1flimlem  23534  mbfi1flim  23535  mbfmul  23538  itg2uba  23555  itg2mulclem  23558  itg2mulc  23559  itg2splitlem  23560  itg2monolem1  23562  itg2i1fseq  23567  itg2gt0  23572  itg2cnlem1  23573  itg2cnlem2  23574  i1fibl  23619  itgitg1  23620  iblabslem  23639  iblabs  23640  bddmulibl  23650  cnplimc  23696  limccnp  23700  limccnp2  23701  dvcnp2  23728  dvmulf  23751  dvcmulf  23753  dvcobr  23754  dvcof  23756  dvcjbr  23757  dvcj  23758  dvfre  23759  dvmptcj  23776  dvcnvlem  23784  dvcnv  23785  dvef  23788  dvsincos  23789  rolle  23798  cmvth  23799  dvlip  23801  dvlipcn  23802  dv11cn  23809  dvivthlem1  23816  dvivth  23818  lhop2  23823  dvfsumrlim2  23840  ftc1lem1  23843  ftc1lem2  23844  ftc1a  23845  ftc1lem4  23847  ftc2  23852  ftc2ditglem  23853  ftc2ditg  23854  tdeglem4  23865  tdeglem2  23866  mdegle0  23882  mdegmullem  23883  plypf1  24013  plyco  24042  dgrcolem1  24074  dgrcolem2  24075  dgrco  24076  plycjlem  24077  dvply2g  24085  plydiveu  24098  elqaalem3  24121  taylthlem1  24172  taylthlem2  24173  ulmshft  24189  ulmdvlem1  24199  mtest  24203  mtestbdd  24204  mbfulm  24205  iblulm  24206  itgulm  24207  pserulm  24221  pserdv  24228  abelthlem1  24230  abelthlem3  24232  pige3  24314  eff1olem  24339  logcn  24438  advlog  24445  advlogexp  24446  logtayl  24451  logccv  24454  dvcxp1  24526  dvcxp2  24527  dvcncxp1  24529  resqrtcn  24535  sqrtcn  24536  loglesqrt  24544  dvatan  24707  leibpi  24714  divsqrtsumo1  24755  jensenlem2  24759  amgmlem  24761  lgamgulmlem2  24801  lgamcvg2  24826  ftalem7  24850  basellem9  24860  muinv  24964  dchrmulid2  25022  dchrinvcl  25023  lgseisenlem4  25148  dchrisum0lem2a  25251  logdivsum  25267  mulog2sumlem1  25268  log2sumbnd  25278  hilnormi  28148  chscllem4  28627  hmopidmchi  29138  rabfodom  29470  ofoprabco  29592  fpwrelmapffslem  29635  fpwrelmap  29636  qqhre  30192  prodindf  30213  esumpcvgval  30268  ofcfval4  30295  omssubadd  30490  carsggect  30508  plymulx0  30752  fdvneggt  30806  fdvnegge  30808  itgexpif  30812  ptpconn  31341  cvmliftlem6  31398  cvmliftlem8  31400  cvmlift2lem7  31417  cvmliftphtlem  31425  cvmlift3lem5  31431  elmsubrn  31551  knoppcnlem9  32616  curunc  33521  poimir  33572  broucube  33573  mblfinlem2  33577  volsupnfl  33584  cnambfre  33588  dvtan  33590  itg2addnclem  33591  itg2addnclem2  33592  itg2addnclem3  33593  itg2addnc  33594  itg2gt0cn  33595  itgaddnc  33600  itgmulc2nc  33608  bddiblnc  33610  ftc1cnnclem  33613  ftc1anclem1  33615  ftc1anclem2  33616  ftc1anclem3  33617  ftc1anclem4  33618  ftc1anclem5  33619  ftc1anclem6  33620  ftc1anclem7  33621  ftc1anclem8  33622  ftc1anc  33623  ftc2nc  33624  upixp  33654  mzpsubst  37628  diophun  37654  mendlmod  38080  mendassa  38081  fsovcnvlem  38624  binomcxplemnotnn0  38872  rnsnf  39684  cncfmptss  40137  climliminflimsupd  40351  mulcncff  40399  subcncff  40411  cncfcompt  40414  addcncff  40415  divcncff  40422  cncfiooicclem1  40424  dvsinexp  40443  dvsubf  40446  dvdivf  40455  dvcosax  40459  dvnmul  40476  dvnprodlem1  40479  dvnprodlem2  40480  itgsinexplem1  40487  itgsubsticclem  40509  iblcncfioo  40512  itgiccshift  40514  stoweidlem20  40555  dirkercncflem2  40639  fourierdlem16  40658  fourierdlem21  40663  fourierdlem22  40664  fourierdlem28  40670  fourierdlem39  40681  fourierdlem51  40692  fourierdlem60  40701  fourierdlem61  40702  fourierdlem69  40710  fourierdlem72  40713  fourierdlem73  40714  fourierdlem81  40722  fourierdlem83  40724  fourierdlem84  40725  fourierdlem87  40728  fourierdlem90  40731  fourierdlem93  40734  fourierdlem95  40736  fourierdlem101  40742  fourierdlem103  40744  fourierdlem104  40745  fourierdlem111  40752  etransclem34  40803  etransclem43  40812  etransclem46  40815  sge0tsms  40915  sge0fodjrnlem  40951  sge0iun  40954  sge0isum  40962  sge0seq  40981  meadjun  40997  meadjiunlem  41000  meadjiun  41001  ismeannd  41002  psmeasurelem  41005  omeiunle  41052  ovn02  41103  smfpimioo  41315  smfresal  41316  smfinflem  41344  smflimsuplem3  41349  smfliminflem  41357  aacllem  42875  amgmwlem  42876  amgmlemALT  42877
  Copyright terms: Public domain W3C validator