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

Theorem ffnd 6505
Description: A mapping is a function with domain, deduction form. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
Hypothesis
Ref Expression
ffnd.1 (𝜑𝐹:𝐴𝐵)
Assertion
Ref Expression
ffnd (𝜑𝐹 Fn 𝐴)

Proof of Theorem ffnd
StepHypRef Expression
1 ffnd.1 . 2 (𝜑𝐹:𝐴𝐵)
2 ffn 6504 . 2 (𝐹:𝐴𝐵𝐹 Fn 𝐴)
31, 2syl 17 1 (𝜑𝐹 Fn 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   Fn wfn 6339  wf 6340
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 210  df-an 400  df-f 6348
This theorem is referenced by:  fnconstg  6558  f1fn  6567  fofn  6584  f1ofn  6608  feqmptd  6725  fprb  6948  rnmptcOLD  6962  cocan1  7040  oprres  7311  off  7419  ofco  7424  caofref  7430  caofid0l  7432  caofid0r  7433  caofid1  7434  caofid2  7435  caofrss  7437  caoftrn  7439  fo2ndf  7814  fnwelem  7822  fnse  7824  suppsnop  7841  suppss  7857  suppssr  7858  suppssof1  7860  suppofssd  7864  suppofss1d  7865  suppofss2d  7866  smorndom  8002  elmapfn  8426  ralxpmap  8457  omxpenlem  8615  mapen  8679  f1finf1o  8743  unirnffid  8814  fdmfifsupp  8841  mapfien  8869  intrnfi  8878  marypha2  8901  ordtypelem7  8986  wemapsolem  9012  wemapso  9013  wemapso2lem  9014  unxpwdom2  9050  ixpiunwdom  9052  cantnfle  9132  cantnfp1lem2  9140  cantnfp1lem3  9141  cantnfp1  9142  oemapvali  9145  cantnflem1a  9146  cantnflem1c  9148  cantnflem3  9152  cantnf  9154  cnfcomlem  9160  cnfcom3  9165  updjudhcoinlf  9359  updjudhcoinrg  9360  fseqenlem1  9449  numacn  9474  infpwfien  9487  isf32lem2  9775  isf34lem7  9800  isf34lem6  9801  unirnfdomd  9988  ofsubeq0  11634  ofnegsub  11635  ofsubge0  11636  seqf1olem2  13418  resunimafz0  13811  wrdfn  13883  swrdvalfn  14016  pfxfn  14046  pfxid  14049  cats1un  14086  cshwfn  14166  ccatco  14200  limsupgle  14837  o1of2  14972  o1rlimmul  14978  isercolllem2  15025  isercoll  15027  isercoll2  15028  climsup  15029  fsumss  15085  ruclem11  15596  vdwlem2  16319  vdwlem6  16323  vdwlem9  16326  vdwlem12  16329  0ram  16357  ramub1lem1  16363  pwsle  16768  pwsleval  16769  pwsvscaval  16771  mrcuni  16895  mrcun  16896  invf1o  17042  funcres2c  17174  setcmon  17350  setcepi  17351  uncfcurf  17492  yoniso  17538  isacs4lem  17781  acsmapd  17791  gsumval2  17899  prdsplusgcl  17945  prdsidlem  17946  prdsmndd  17947  mhmf1o  17969  resmhm2b  17990  mhmima  17992  mhmeql  17993  prdspjmhm  17996  pwsco1mhm  17999  pwsco2mhm  18000  gsumwmhm  18013  frmdss2  18031  grpinvf1o  18172  prdsinvlem  18211  cycsubgcl  18352  ghmrn  18374  ghmpreima  18383  ghmeql  18384  ghmnsgima  18385  ghmnsgpreima  18386  ghmeqker  18388  ghmf1o  18391  gass  18434  cntzmhm  18472  symgextres  18556  gsmsymgrfixlem1  18558  fvcosymgeq  18560  f1omvdconj  18577  pmtrfinv  18592  symgtrinv  18603  pmtr3ncomlem1  18604  sygbasnfpfi  18643  efginvrel2  18856  efgredleme  18872  ghmplusg  18969  prdscmnd  18984  gsumval3a  19026  gsumval3eu  19027  gsumzaddlem  19044  gsumzsplit  19050  gsumpt  19085  prdsgsum  19104  dprdfcntz  19140  dprdfadd  19145  dprdfeq0  19147  dprdf11  19148  dprdlub  19151  dprdspan  19152  dprd2dlem1  19166  dmdprdpr  19174  dprdpr  19175  dpjlem  19176  ablfac1eu  19198  prdsmulrcl  19367  prdsringd  19368  prdscrngd  19369  prds1  19370  rhmf1o  19490  rnrhmsubrg  19570  isabvd  19594  lmodfopnelem1  19673  lcomfsupp  19677  prdsvscacl  19743  prdslmodd  19744  lmhmco  19818  lmhmplusg  19819  lmhmvsca  19820  lmhmf1o  19821  lmhmeql  19830  lspextmo  19831  rrgsupp  20067  psrbaglesupp  20151  psrbagcon  20154  psrbaglefi  20155  psrbagconf1o  20157  gsumbagdiaglem  20158  psrvscaval  20175  psrlidm  20186  psrridm  20187  psrass1  20188  psrdi  20189  psrdir  20190  mplsubglem  20217  mplvscaval  20231  subrgmvrf  20246  mplbas2  20254  mvrf2  20275  mplind  20285  psrbagev1  20293  evlslem3  20296  evlslem1  20298  evlsvar  20306  mpfind  20323  mhpinvcl  20342  psrplusgpropd  20407  coe1add  20435  coe1addfv  20436  evl1addd  20507  evl1subd  20508  evl1muld  20509  pf1mpf  20518  pf1ind  20521  pjfo  20862  dsmmbas2  20884  dsmm0cl  20887  dsmmacl  20888  dsmmsubg  20890  dsmmlss  20891  frlmvplusgvalc  20914  frlmvscaval  20915  frlmplusgvalb  20916  frlmvscavalb  20917  frlmsslss2  20922  frlmphllem  20927  frlmphl  20928  frlmssuvc2  20942  frlmsslsp  20943  frlmup1  20945  frlmup2  20946  frlmup3  20947  frlmup4  20948  islindf4  20985  mamudir  21016  mamulid  21053  mamurid  21054  mdetrlin  21214  mdetrsca  21215  mdetralt  21220  mdetunilem7  21230  mdetunilem9  21232  madurid  21256  cnrest2  21897  lmss  21909  lmcnp  21915  cnt0  21957  cnt1  21961  cnhaus  21965  rncmp  22007  conncn  22037  2ndcomap  22069  1stccnp  22073  comppfsc  22143  1stckgenlem  22164  ptbasfi  22192  ptopn  22194  ptclsg  22226  ptcnp  22233  upxp  22234  txtube  22251  txcmplem1  22252  hauseqlcld  22257  xkohaus  22264  xkoptsub  22265  cnmpt11  22274  cnmpt21  22282  cnmpt22f  22286  cnmptcom  22289  qtopss  22326  qtopeu  22327  qtopomap  22329  qtopcmap  22330  kqffn  22336  hmeof1o2  22374  xkocnv  22425  rnelfm  22564  ptcmplem1  22663  cnextfres1  22679  ghmcnp  22726  tgphaus  22728  prdstmdd  22735  prdstgpd  22736  fmucnd  22904  psmetxrge0  22926  isxmet2d  22940  prdsmet  22983  blelrnps  23029  blelrn  23030  xmetresbl  23050  comet  23126  stdbdxmet  23128  met2ndci  23135  prdsxmslem2  23142  isngp3  23210  nmotri  23351  metdsre  23464  bndth  23569  evth  23570  fmcfil  23882  bcthlem4  23937  rrxcph  24002  rrxds  24003  rrxmet  24018  evthicc2  24070  ovolfsf  24081  ovolmge0  24087  ovollb2lem  24098  ovolunlem1a  24106  ovoliunlem1  24112  ovoliun  24115  ovoliun2  24116  ovolscalem1  24123  ovolicc1  24126  ovolicc2lem4  24130  ovolicc2  24132  voliunlem1  24160  voliunlem3  24162  volsup  24166  ioombl1lem2  24169  ioombl1lem4  24171  uniiccdif  24188  uniioombllem2  24193  uniioombllem3  24195  uniioombllem6  24198  volsup2  24215  vitalilem4  24221  mbfeqalem1  24251  mbfmulc2lem  24257  mbfmax  24259  mbfaddlem  24270  mbfadd  24271  mbfsub  24272  mbfsup  24274  mbfinf  24275  itg1ge0  24296  itg1addlem1  24302  i1faddlem  24303  i1fmullem  24304  i1fadd  24305  i1fmul  24306  itg1addlem4  24309  i1fmulclem  24312  i1fmulc  24313  itg1mulc  24314  i1fres  24315  itg10a  24320  itg1ge0a  24321  itg1lea  24322  mbfi1fseqlem3  24327  mbfi1fseqlem4  24328  mbfi1flimlem  24332  mbfmullem2  24334  mbfmul  24336  itg20  24347  itg2lea  24354  itg2splitlem  24358  itg2split  24359  itg2monolem1  24360  itg2monolem2  24361  itg2monolem3  24362  itg2mono  24363  itg2i1fseqle  24364  itg2i1fseq  24365  itg2addlem  24368  itg2gt0  24370  itg2cnlem1  24371  itg2cnlem2  24372  itg2cn  24373  itgitg1  24418  bddmulibl  24448  bddibl  24449  dvidlem  24524  dvaddbr  24547  dvmulbr  24548  dvaddf  24551  dvcmulf  24554  dvrec  24564  dvcnvlem  24585  rolle  24599  dveq0  24609  dv11cn  24610  dvivthlem2  24618  dvivth  24619  dvne0  24620  lhop1lem  24622  lhop1  24623  lhop2  24624  lhop  24625  ftc1cn  24652  tdeglem4  24667  mdegleb  24671  mdegldg  24673  mdegaddle  24681  ply1remlem  24769  ply1rem  24770  fta1glem1  24772  fta1glem2  24773  fta1blem  24775  plyeq0lem  24813  plyeq0  24814  plyaddlem1  24816  coeeulem  24827  coeaddlem  24852  coemulc  24858  dgradd2  24871  dgrcolem2  24877  ofmulrt  24884  plyrem  24907  vieta1lem1  24912  vieta1  24914  plyexmo  24915  elqaalem3  24923  aannenlem1  24930  aalioulem2  24935  ulmuni  24993  ulmdvlem1  25001  ulmdv  25004  mbfulm  25007  iblulm  25008  itgulm  25009  rlimcnp2  25558  jensen  25580  amgm  25582  basellem3  25674  basellem7  25678  basellem9  25680  dchrelbas2  25827  dchrmulcl  25839  dchrfi  25845  dchreq  25848  dchrresb  25849  dchrinv  25851  dchr1re  25853  sumdchr2  25860  dchr2sum  25863  lgsqrlem2  25937  lgsqrlem3  25938  rpvmasum2  26102  dchrisum0re  26103  mirf1o  26469  lmif1o  26595  eqeefv  26703  axlowdimlem14  26755  vtxdgfisf  27272  2pthon3v  27735  nvinvfval  28429  sspg  28517  ssps  28519  sspmlem  28521  sspn  28525  lnon0  28587  ubthlem1  28659  pjfn  29498  kbpj  29745  kbass2  29906  elpjrn  29979  ofrn2  30401  off2  30402  ofresid  30403  xppreima2  30409  ofpreima2  30425  suppovss  30440  resf1o  30480  swrdrn3  30643  pwrssmgc  30694  gsumle  30760  symgcom2  30763  pmtrcnel  30768  pmtrcnel2  30769  pmtrcnelor  30770  cycpmfvlem  30789  cycpmfv3  30792  cycpmcl  30793  cycpmco2rn  30802  cycpmco2  30810  cycpm3cl2  30813  cyc3co2  30817  cyc3evpm  30827  islinds5  30968  ellspds  30969  dimkerim  31086  fedgmullem2  31089  fedgmul  31090  cmpcref  31177  fsumcvg4  31253  pl1cn  31258  qqhval2lem  31282  prodindf  31342  indpreima  31344  esumcvg  31405  ofcf  31422  ofcof  31426  measfn  31523  meascnbl  31538  sibfof  31658  sitgaddlemb  31666  subiwrdlen  31704  rrvfn  31763  plymul02  31876  signsplypnf  31880  signsply0  31881  reprsuc  31946  reprdifc  31958  breprexplema  31961  circlemethhgt  31974  hgt750lemb  31987  f1resrcmplf1dlem  32419  pthhashvtx  32434  cvmopnlem  32585  cvmliftmolem1  32588  cvmliftlem10  32601  cvmlift2lem9a  32610  cvmlift2lem6  32615  cvmlift2lem12  32621  cvmliftphtlem  32624  cvmlift3lem9  32634  mrsubrn  32820  elmrsubrn  32827  elmsubrn  32835  msubrn  32836  mclsind  32877  mclsppslem  32890  mclspps  32891  iprodefisumlem  33032  matunitlindflem1  34999  poimirlem1  35004  poimirlem2  35005  poimirlem3  35006  poimirlem16  35019  poimirlem17  35020  poimirlem19  35022  poimirlem20  35023  poimirlem22  35025  poimirlem23  35026  poimirlem29  35032  poimirlem30  35033  poimirlem31  35034  poimir  35036  mblfinlem2  35041  itg2addnclem3  35056  itg2addnc  35057  itg2gt0cn  35058  ftc1cnnc  35075  ftc1anclem5  35080  ftc1anclem7  35082  ftc1anc  35084  sdclem2  35126  istotbnd3  35155  sstotbnd2  35158  isbnd3  35168  heibor1lem  35193  rrnmet  35213  grpokerinj  35277  isdrngo2  35342  lfl1  36312  lfladdcl  36313  lflvscl  36319  lkr0f  36336  lkrsc  36339  eqlkr2  36342  eqlkr3  36343  ldualvaddval  36373  ldualvsval  36380  tendoeq1  38006  metakunt19  39315  metakunt25  39321  frlmvscadiccat  39374  frlmsnic  39388  ismrcd1  39556  ismrcd2  39557  istopclsd  39558  isnacs3  39568  mzpaddmpt  39599  mzpmulmpt  39600  mzpsubst  39606  mzpcong  39830  fnwe2lem2  39912  islmodfg  39930  kercvrlsm  39944  dgrsub2  39996  mpaaeu  40011  rngunsnply  40034  idomrootle  40056  hausgraph  40073  fsovf1od  40635  brcoffn  40653  clsneiel1  40731  wfximgfd  40787  extoimad  40788  mnringmulrcld  40857  mnurndlem1  40910  caofcan  40948  ofmul12  40950  ofdivrec  40951  ofdivcan4  40952  ofdivdiv2  40953  dvconstbi  40959  binomcxplemnotnn0  40981  refsum2cnlem1  41587  ssmapsn  41771  preimaiocmnf  42125  fsumsupp0  42147  fsumsermpt  42148  climinf  42175  climinf2lem  42275  limsupmnflem  42289  limsupvaluz2  42307  supcnvlimsup  42309  limsupgtlem  42346  liminfvalxr  42352  liminflelimsupuz  42354  xlimconst2  42404  climxlim2  42415  icccncfext  42456  dvnprodlem1  42515  volicoff  42564  voliooicof  42565  fourierdlem25  42701  etransclem2  42805  etransclem35  42838  fge0iccico  42936  sge0tsms  42946  sge0sup  42957  sge0resrn  42970  sge0le  42973  sge0fodjrnlem  42982  sge0isum  42993  sge0seq  43012  nnfoctbdjlem  43021  meadjiunlem  43031  omeiunle  43083  hoicvr  43114  ovolval4lem1  43215  ovolval5lem3  43220  ovnovollem1  43222  ovnovollem2  43223  iinhoiicclem  43239  iunhoiioolem  43241  preimaicomnf  43274  smfresal  43347  smfsuplem1  43369  smflimsuplem2  43379  mgmhmf1o  44334  resmgmhm2b  44347  mgmhmima  44349  mgmhmeql  44350  rnghmf1o  44454  ackvalsucsucval  45029  amgmwlem  45257
  Copyright terms: Public domain W3C validator