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

Theorem feqmptd 6726
Description: Deduction form of dffn5 6717. (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 (𝜑𝐹:𝐴𝐵)
21ffnd 6508 . 2 (𝜑𝐹 Fn 𝐴)
3 dffn5 6717 . 2 (𝐹 Fn 𝐴𝐹 = (𝑥𝐴 ↦ (𝐹𝑥)))
42, 3sylib 219 1 (𝜑𝐹 = (𝑥𝐴 ↦ (𝐹𝑥)))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1528  cmpt 5137   Fn wfn 6343  wf 6344  cfv 6348
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-sep 5194  ax-nul 5201  ax-pr 5320
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2615  df-eu 2647  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-ral 3140  df-rex 3141  df-rab 3144  df-v 3494  df-sbc 3770  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-nul 4289  df-if 4464  df-sn 4558  df-pr 4560  df-op 4564  df-uni 4831  df-br 5058  df-opab 5120  df-mpt 5138  df-id 5453  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-iota 6307  df-fun 6350  df-fn 6351  df-f 6352  df-fv 6356
This theorem is referenced by:  feqresmpt  6727  cofmpt  6886  fcoconst  6888  ofco  7418  caofinvl  7425  caofcom  7430  caofass  7432  caofdi  7434  caofdir  7435  caonncan  7436  suppssof1  7852  mapxpen  8671  xpmapenlem  8672  cantnfp1  9132  cantnflem1  9140  cnfcom2lem  9152  infxpenc  9432  pwfseqlem5  10073  gruf  10221  ccatco  14185  cnrecnv  14512  rlimclim1  14890  rlimuni  14895  lo1resb  14909  rlimresb  14910  o1resb  14911  rlimcn1  14933  rlimo1  14961  o1rlimmul  14963  caucvgr  15020  ackbijnn  15171  bitsf1ocnv  15781  ramcl  16353  pwsplusgval  16751  pwsmulrval  16752  pwsvscafval  16755  setcepi  17336  prf1st  17442  prf2nd  17443  1st2ndprf  17444  curfuncf  17476  curf2ndf  17485  yonedainv  17519  yonffthlem  17520  prdsidlem  17931  pwsco1mhm  17984  pwsco2mhm  17985  frmdup3lem  18019  frmdup3  18020  grpinvcnv  18105  pwsinvg  18150  pwssub  18151  efginvrel1  18783  frgpup3lem  18832  frgpup3  18833  gsumval3  18956  gsumcllem  18957  gsumzf1o  18961  gsumzsplit  18976  gsumconst  18983  gsumzmhm  18986  gsumsub  18997  gsum2dlem2  19020  gsumcom2  19024  dprdfadd  19071  dprdfsub  19072  dprdfeq0  19073  dprdf11  19074  dmdprdsplitlem  19088  dprddisj2  19090  dpjidcl  19109  ablfaclem2  19137  ablfac2  19140  mptscmfsuppd  19629  lmhmvsca  19746  rrgsupp  19992  psrbagaddcl  20078  gsumbagdiaglem  20083  psrass1lem  20085  psrlinv  20105  psrass1  20113  psrcom  20117  mplsubrglem  20147  mplmonmul  20173  mplcoe1  20174  mplcoe5  20177  evlslem2  20220  evlslem6  20222  evlslem1  20223  coe1fval3  20304  coe1sclmul  20378  coe1sclmul2  20380  mulgrhm2  20574  cygznlem2a  20642  frgpcyg  20648  uvcresum  20865  frlmup1  20870  grpvrinv  20935  mhmvlin  20936  mdetleib2  21125  mdetunilem9  21157  cayleyhamilton1  21428  neiptopnei  21668  dfac14  22154  ptcnp  22158  lmcn2  22185  cnmpt11f  22200  cnmpt21f  22208  cnmpt2k  22224  qtopeu  22252  xkocnv  22350  xkohmeo  22351  flfcnp2  22543  istgp2  22627  tmdgsum  22631  symgtgp  22637  subgtgp  22641  tgpconncomp  22648  prdstgpd  22660  tsmssub  22684  tgptsmscls  22685  tsmssplit  22687  tsmsxplem1  22688  tlmtgp  22731  ustuqtop  22782  prdsmslem1  23064  prdsxmslem1  23065  prdsxmslem2  23066  tngnm  23187  nmoeq0  23272  cnfldnm  23314  cncfmpt1f  23448  negfcncf  23454  cnrehmeo  23484  evth  23490  evth2  23491  copco  23549  pcopt  23553  pcopt2  23554  pcoass  23555  pcorev2  23559  pi1xfrcnv  23588  ovolctb  24018  ovolfs2  24099  uniioombllem2  24111  ismbf  24156  mbfconst  24161  mbfmulc2re  24176  mbfadd  24189  mbfsub  24190  mbflimsup  24194  mbfi1flimlem  24250  mbfi1flim  24251  mbfmul  24254  itg2uba  24271  itg2mulclem  24274  itg2mulc  24275  itg2splitlem  24276  itg2monolem1  24278  itg2i1fseq  24283  itg2gt0  24288  itg2cnlem1  24289  itg2cnlem2  24290  i1fibl  24335  itgitg1  24336  bddmulibl  24366  cnplimc  24412  limccnp2  24417  dvcnp2  24444  dvmulf  24467  dvcmulf  24469  dvcobr  24470  dvcof  24472  dvcj  24474  dvfre  24475  dvmptcj  24492  dvcnvlem  24500  dvcnv  24501  dvef  24504  dvsincos  24505  rolle  24514  cmvth  24515  dvlip  24517  dvlipcn  24518  dv11cn  24525  dvivthlem1  24532  dvivth  24534  lhop2  24539  dvfsumrlim2  24556  ftc1lem1  24559  ftc1lem2  24560  ftc1a  24561  ftc1lem4  24563  ftc2  24568  ftc2ditglem  24569  ftc2ditg  24570  tdeglem4  24581  tdeglem2  24582  mdegle0  24598  mdegmullem  24599  plypf1  24729  plyco  24758  dgrcolem1  24790  dgrcolem2  24791  dgrco  24792  plycjlem  24793  dvply2g  24801  plydiveu  24814  elqaalem3  24837  taylthlem1  24888  taylthlem2  24889  ulmshft  24905  ulmdvlem1  24915  mtest  24919  mtestbdd  24920  mbfulm  24921  iblulm  24922  itgulm  24923  pserulm  24937  pserdv  24944  abelthlem1  24946  abelthlem3  24948  pige3ALT  25032  eff1olem  25059  logcn  25157  advlog  25164  advlogexp  25165  logtayl  25170  logccv  25173  dvcxp1  25248  dvcxp2  25249  dvcncxp1  25251  resqrtcn  25257  sqrtcn  25258  loglesqrt  25266  dvatan  25440  leibpi  25447  divsqrtsumo1  25488  jensenlem2  25492  amgmlem  25494  lgamgulmlem2  25534  ftalem7  25583  basellem9  25593  muinv  25697  dchrmulid2  25755  dchrinvcl  25756  dchrisum0lem2a  26020  logdivsum  26036  mulog2sumlem1  26037  log2sumbnd  26047  hilnormi  28867  chscllem4  29344  hmopidmchi  29855  rabfodom  30193  ofoprabco  30337  fpwrelmapffslem  30394  fpwrelmap  30395  lbsdiflsp0  30921  fedgmullem1  30924  qqhre  31160  prodindf  31181  esumpcvgval  31236  ofcfval4  31263  omssubadd  31457  carsggect  31475  plymulx0  31716  fdvneggt  31770  fdvnegge  31772  itgexpif  31776  ptpconn  32377  cvmliftlem6  32434  cvmliftlem8  32436  cvmlift2lem7  32453  cvmliftphtlem  32461  cvmlift3lem5  32467  elmsubrn  32672  knoppcnlem9  33737  curunc  34755  poimir  34806  broucube  34807  mblfinlem2  34811  volsupnfl  34818  cnambfre  34821  dvtan  34823  itg2addnclem  34824  itg2addnclem2  34825  itg2addnclem3  34826  itg2addnc  34827  itg2gt0cn  34828  itgaddnc  34833  itgmulc2nc  34841  bddiblnc  34843  ftc1cnnclem  34846  ftc1anclem1  34848  ftc1anclem2  34849  ftc1anclem3  34850  ftc1anclem4  34851  ftc1anclem5  34852  ftc1anclem6  34853  ftc1anclem7  34854  ftc1anclem8  34855  ftc1anc  34856  ftc2nc  34857  upixp  34885  mzpsubst  39223  diophun  39248  mendlmod  39671  mendassa  39672  fsovcnvlem  40237  binomcxplemnotnn0  40565  rnsnf  41320  cncfmptss  41744  climliminflimsupd  41958  mulcncff  42027  subcncff  42039  cncfcompt  42042  addcncff  42043  divcncff  42050  cncfiooicclem1  42052  dvsinexp  42071  dvsubf  42074  dvdivf  42083  dvcosax  42087  dvnmul  42104  dvnprodlem1  42107  dvnprodlem2  42108  itgsinexplem1  42115  itgsubsticclem  42136  iblcncfioo  42139  itgiccshift  42141  stoweidlem20  42182  dirkercncflem2  42266  fourierdlem16  42285  fourierdlem21  42290  fourierdlem22  42291  fourierdlem28  42297  fourierdlem39  42308  fourierdlem51  42319  fourierdlem60  42328  fourierdlem61  42329  fourierdlem69  42337  fourierdlem72  42340  fourierdlem73  42341  fourierdlem81  42349  fourierdlem83  42351  fourierdlem84  42352  fourierdlem87  42355  fourierdlem90  42358  fourierdlem93  42361  fourierdlem95  42363  fourierdlem101  42369  fourierdlem103  42371  fourierdlem104  42372  fourierdlem111  42379  etransclem34  42430  etransclem43  42439  etransclem46  42442  sge0tsms  42539  sge0fodjrnlem  42575  sge0iun  42578  sge0isum  42586  sge0seq  42605  meadjun  42621  meadjiunlem  42624  meadjiun  42625  ismeannd  42626  psmeasurelem  42629  omeiunle  42676  ovn02  42727  smfpimioo  42939  smfresal  42940  smfinflem  42968  smflimsuplem3  42973  smfliminflem  42981  aacllem  44830  amgmwlem  44831  amgmlemALT  44832
  Copyright terms: Public domain W3C validator