Theorem ffnd 6585

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

Step	Hyp	Ref	Expression
1		ffnd.1	. 2 ⊢ (𝜑 → 𝐹:𝐴⟶𝐵)
2		ffn 6584	. 2 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴)
3	1, 2	syl 17	1 ⊢ (𝜑 → 𝐹 Fn 𝐴)

Syntax hints:   → wi 4   Fn wfn 6413  ⟶wf 6414

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 206  df-an 396  df-f 6422

This theorem is referenced by:  fnconstg  6646  f1fn  6655  fofn  6674  f1ofn  6701  feqmptd  6819  fprb  7051  rnmptcOLD  7065  cocan1  7143  oprres  7418  off  7529  ofco  7534  caofref  7540  caofid0l  7542  caofid0r  7543  caofid1  7544  caofid2  7545  caofrss  7547  caoftrn  7549  fo2ndf  7933  fnwelem  7943  fnse  7945  suppsnop  7965  suppss  7981  suppssOLD  7982  suppssr  7983  suppssrg  7984  suppssof1  7986  suppofssd  7990  suppofss1d  7991  suppofss2d  7992  suppcoss  7994  smorndom  8170  elmapfn  8611  ralxpmap  8642  omxpenlem  8813  mapen  8877  f1finf1o  8975  unirnffid  9041  fdmfifsupp  9068  mapfien  9097  intrnfi  9105  marypha2  9128  ordtypelem7  9213  wemapsolem  9239  wemapso  9240  wemapso2lem  9241  unxpwdom2  9277  ixpiunwdom  9279  cantnfle  9359  cantnfp1lem2  9367  cantnfp1lem3  9368  cantnfp1  9369  oemapvali  9372  cantnflem1a  9373  cantnflem1c  9375  cantnflem3  9379  cantnf  9381  cnfcomlem  9387  cnfcom3  9392  updjudhcoinlf  9621  updjudhcoinrg  9622  fseqenlem1  9711  numacn  9736  infpwfien  9749  isf32lem2  10041  isf34lem7  10066  isf34lem6  10067  unirnfdomd  10254  ofsubeq0  11900  ofnegsub  11901  ofsubge0  11902  seqf1olem2  13691  resunimafz0  14085  wrdfn  14159  swrdvalfn  14292  pfxfn  14322  pfxid  14325  cats1un  14362  cshwfn  14442  ccatco  14476  limsupgle  15114  o1of2  15250  o1rlimmul  15256  isercolllem2  15305  isercoll  15307  isercoll2  15308  climsup  15309  fsumss  15365  ruclem11  15877  vdwlem2  16611  vdwlem6  16615  vdwlem9  16618  vdwlem12  16621  0ram  16649  ramub1lem1  16655  pwsle  17120  pwsleval  17121  pwsvscaval  17123  mrcuni  17247  mrcun  17248  invf1o  17398  funcres2c  17533  setcmon  17718  setcepi  17719  uncfcurf  17873  yoniso  17919  isacs4lem  18177  acsmapd  18187  gsumval2  18285  prdsplusgcl  18331  prdsidlem  18332  prdsmndd  18333  mhmf1o  18355  resmhm2b  18376  mhmima  18378  mhmeql  18379  prdspjmhm  18382  pwsco1mhm  18385  pwsco2mhm  18386  gsumwmhm  18399  frmdss2  18417  grpinvf1o  18560  prdsinvlem  18599  cycsubgcl  18740  ghmrn  18762  ghmpreima  18771  ghmeql  18772  ghmnsgima  18773  ghmnsgpreima  18774  ghmeqker  18776  ghmf1o  18779  gass  18822  cntzmhm  18860  symgextres  18948  gsmsymgrfixlem1  18950  fvcosymgeq  18952  f1omvdconj  18969  pmtrfinv  18984  symgtrinv  18995  pmtr3ncomlem1  18996  sygbasnfpfi  19035  efginvrel2  19248  efgredleme  19264  ghmplusg  19362  prdscmnd  19377  gsumval3a  19419  gsumval3eu  19420  gsumzaddlem  19437  gsumzsplit  19443  gsumpt  19478  prdsgsum  19497  dprdfcntz  19533  dprdfadd  19538  dprdfeq0  19540  dprdf11  19541  dprdlub  19544  dprdspan  19545  dprd2dlem1  19559  dmdprdpr  19567  dprdpr  19568  dpjlem  19569  ablfac1eu  19591  prdsmulrcl  19765  prdsringd  19766  prdscrngd  19767  prds1  19768  rhmf1o  19891  rnrhmsubrg  19971  isabvd  19995  lmodfopnelem1  20074  lcomfsupp  20078  prdsvscacl  20145  prdslmodd  20146  lmhmco  20220  lmhmplusg  20221  lmhmvsca  20222  lmhmf1o  20223  lmhmeql  20232  lspextmo  20233  rrgsupp  20475  pjfo  20832  dsmmbas2  20854  dsmm0cl  20857  dsmmacl  20858  dsmmsubg  20860  dsmmlss  20861  frlmvplusgvalc  20884  frlmvscaval  20885  frlmplusgvalb  20886  frlmvscavalb  20887  frlmsslss2  20892  frlmphllem  20897  frlmphl  20898  frlmssuvc2  20912  frlmsslsp  20913  frlmup1  20915  frlmup2  20916  frlmup3  20917  frlmup4  20918  islindf4  20955  psrbagfsupp  21033  psrbaglesupp  21037  psrbaglesuppOLD  21038  psrbaglecl  21039  psrbagaddcl  21041  psrbagcon  21043  psrbagconOLD  21044  psrbaglefi  21045  psrbaglefiOLD  21046  psrbagconf1o  21049  psrbagconf1oOLD  21050  gsumbagdiaglemOLD  21051  gsumbagdiaglem  21054  psrass1lem  21056  psrvscaval  21071  psrlidm  21082  psrridm  21083  psrass1  21084  psrdi  21085  psrdir  21086  mplsubglem  21115  mplvscaval  21130  subrgmvrf  21145  mplbas2  21153  mvrf2  21178  mplind  21188  psrbagev1  21195  psrbagev1OLD  21196  psrbagev2  21197  evlslem3  21200  evlslem1  21202  evlsvar  21210  mpfind  21227  ismhp3  21243  mhpmulcl  21249  psrplusgpropd  21317  coe1add  21345  coe1addfv  21346  evl1addd  21417  evl1subd  21418  evl1muld  21419  pf1mpf  21428  pf1ind  21431  mamudir  21461  mamulid  21498  mamurid  21499  mdetrlin  21659  mdetrsca  21660  mdetralt  21665  mdetunilem7  21675  mdetunilem9  21677  madurid  21701  cnrest2  22345  lmss  22357  lmcnp  22363  cnt0  22405  cnt1  22409  cnhaus  22413  rncmp  22455  conncn  22485  2ndcomap  22517  1stccnp  22521  comppfsc  22591  1stckgenlem  22612  ptbasfi  22640  ptopn  22642  ptclsg  22674  ptcnp  22681  upxp  22682  txtube  22699  txcmplem1  22700  hauseqlcld  22705  xkohaus  22712  xkoptsub  22713  cnmpt11  22722  cnmpt21  22730  cnmpt22f  22734  cnmptcom  22737  qtopss  22774  qtopeu  22775  qtopomap  22777  qtopcmap  22778  kqffn  22784  hmeof1o2  22822  xkocnv  22873  rnelfm  23012  ptcmplem1  23111  cnextfres1  23127  ghmcnp  23174  tgphaus  23176  prdstmdd  23183  prdstgpd  23184  fmucnd  23352  psmetxrge0  23374  isxmet2d  23388  prdsmet  23431  blelrnps  23477  blelrn  23478  xmetresbl  23498  comet  23575  stdbdxmet  23577  met2ndci  23584  prdsxmslem2  23591  isngp3  23660  nmotri  23809  metdsre  23922  bndth  24027  evth  24028  fmcfil  24341  bcthlem4  24396  rrxcph  24461  rrxds  24462  rrxmet  24477  evthicc2  24529  ovolfsf  24540  ovolmge0  24546  ovollb2lem  24557  ovolunlem1a  24565  ovoliunlem1  24571  ovoliun  24574  ovoliun2  24575  ovolscalem1  24582  ovolicc1  24585  ovolicc2lem4  24589  ovolicc2  24591  voliunlem1  24619  voliunlem3  24621  volsup  24625  ioombl1lem2  24628  ioombl1lem4  24630  uniiccdif  24647  uniioombllem2  24652  uniioombllem3  24654  uniioombllem6  24657  volsup2  24674  vitalilem4  24680  mbfeqalem1  24710  mbfmulc2lem  24716  mbfmax  24718  mbfaddlem  24729  mbfadd  24730  mbfsub  24731  mbfsup  24733  mbfinf  24734  itg1ge0  24755  itg1addlem1  24761  i1faddlem  24762  i1fmullem  24763  i1fadd  24764  i1fmul  24765  itg1addlem4  24768  itg1addlem4OLD  24769  i1fmulclem  24772  i1fmulc  24773  itg1mulc  24774  i1fres  24775  itg10a  24780  itg1ge0a  24781  itg1lea  24782  mbfi1fseqlem3  24787  mbfi1fseqlem4  24788  mbfi1flimlem  24792  mbfmullem2  24794  mbfmul  24796  itg20  24807  itg2lea  24814  itg2splitlem  24818  itg2split  24819  itg2monolem1  24820  itg2monolem2  24821  itg2monolem3  24822  itg2mono  24823  itg2i1fseqle  24824  itg2i1fseq  24825  itg2addlem  24828  itg2gt0  24830  itg2cnlem1  24831  itg2cnlem2  24832  itg2cn  24833  itgitg1  24878  bddmulibl  24908  bddibl  24909  dvidlem  24984  dvaddbr  25007  dvmulbr  25008  dvaddf  25011  dvcmulf  25014  dvrec  25024  dvcnvlem  25045  rolle  25059  dveq0  25069  dv11cn  25070  dvivthlem2  25078  dvivth  25079  dvne0  25080  lhop1lem  25082  lhop1  25083  lhop2  25084  lhop  25085  ftc1cn  25112  tdeglem1  25125  tdeglem3  25127  tdeglem4  25129  tdeglem4OLD  25130  mdegleb  25134  mdegldg  25136  mdegaddle  25144  ply1remlem  25232  ply1rem  25233  fta1glem1  25235  fta1glem2  25236  fta1blem  25238  plyeq0lem  25276  plyeq0  25277  plyaddlem1  25279  coeeulem  25290  coeaddlem  25315  coemulc  25321  dgradd2  25334  dgrcolem2  25340  ofmulrt  25347  plyrem  25370  vieta1lem1  25375  vieta1  25377  plyexmo  25378  elqaalem3  25386  aannenlem1  25393  aalioulem2  25398  ulmuni  25456  ulmdvlem1  25464  ulmdv  25467  mbfulm  25470  iblulm  25471  itgulm  25472  rlimcnp2  26021  jensen  26043  amgm  26045  basellem3  26137  basellem7  26141  basellem9  26143  dchrelbas2  26290  dchrmulcl  26302  dchrfi  26308  dchreq  26311  dchrresb  26312  dchrinv  26314  dchr1re  26316  sumdchr2  26323  dchr2sum  26326  lgsqrlem2  26400  lgsqrlem3  26401  rpvmasum2  26565  dchrisum0re  26566  mirf1o  26934  lmif1o  27060  eqeefv  27174  axlowdimlem14  27226  vtxdgfisf  27746  2pthon3v  28209  nvinvfval  28903  sspg  28991  ssps  28993  sspmlem  28995  sspn  28999  lnon0  29061  ubthlem1  29133  pjfn  29972  kbpj  30219  kbass2  30380  elpjrn  30453  ofrn2  30878  off2  30879  ofresid  30880  xppreima2  30889  ofpreima2  30905  suppovss  30919  resf1o  30967  swrdrn3  31129  pwrssmgc  31180  mgcf1o  31183  gsumhashmul  31218  gsumle  31252  symgcom2  31255  pmtrcnel  31260  pmtrcnel2  31261  pmtrcnelor  31262  cycpmfvlem  31281  cycpmfv3  31284  cycpmcl  31285  cycpmco2rn  31294  cycpmco2  31302  cycpm3cl2  31305  cyc3co2  31309  cyc3evpm  31319  islinds5  31465  ellspds  31466  rhmpreimaidl  31505  elrspunidl  31508  rhmimaidl  31511  rhmpreimaprmidl  31529  dimkerim  31610  fedgmullem2  31613  fedgmul  31614  cmpcref  31702  rhmpreimacnlem  31736  fsumcvg4  31802  pl1cn  31807  qqhval2lem  31831  prodindf  31891  indpreima  31893  esumcvg  31954  ofcf  31971  ofcof  31975  measfn  32072  meascnbl  32087  sibfof  32207  sitgaddlemb  32215  subiwrdlen  32253  rrvfn  32312  plymul02  32425  signsplypnf  32429  signsply0  32430  reprsuc  32495  reprdifc  32507  breprexplema  32510  circlemethhgt  32523  hgt750lemb  32536  f1resrcmplf1dlem  32958  pthhashvtx  32989  cvmopnlem  33140  cvmliftmolem1  33143  cvmliftlem10  33156  cvmlift2lem9a  33165  cvmlift2lem6  33170  cvmlift2lem12  33176  cvmliftphtlem  33179  cvmlift3lem9  33189  mrsubrn  33375  elmrsubrn  33382  elmsubrn  33390  msubrn  33391  mclsind  33432  mclsppslem  33445  mclspps  33446  iprodefisumlem  33612  matunitlindflem1  35700  poimirlem1  35705  poimirlem2  35706  poimirlem3  35707  poimirlem16  35720  poimirlem17  35721  poimirlem19  35723  poimirlem20  35724  poimirlem22  35726  poimirlem23  35727  poimirlem29  35733  poimirlem30  35734  poimirlem31  35735  poimir  35737  mblfinlem2  35742  itg2addnclem3  35757  itg2addnc  35758  itg2gt0cn  35759  ftc1cnnc  35776  ftc1anclem5  35781  ftc1anclem7  35783  ftc1anc  35785  sdclem2  35827  istotbnd3  35856  sstotbnd2  35859  isbnd3  35869  heibor1lem  35894  rrnmet  35914  grpokerinj  35978  isdrngo2  36043  lfl1  37011  lfladdcl  37012  lflvscl  37018  lkr0f  37035  lkrsc  37038  eqlkr2  37041  eqlkr3  37042  ldualvaddval  37072  ldualvsval  37079  tendoeq1  38705  sticksstones1  40030  sticksstones2  40031  sticksstones3  40032  sticksstones12a  40041  sticksstones12  40042  metakunt19  40071  metakunt25  40077  metakunt33  40085  frlmvscadiccat  40163  frlmsnic  40188  pwspjmhmmgpd  40192  pwsgprod  40194  evlsbagval  40198  evlsaddval  40200  evlsmulval  40201  fsuppssind  40205  mhphf  40208  ismrcd1  40436  ismrcd2  40437  istopclsd  40438  isnacs3  40448  mzpaddmpt  40479  mzpmulmpt  40480  mzpsubst  40486  mzpcong  40710  fnwe2lem2  40792  islmodfg  40810  kercvrlsm  40824  dgrsub2  40876  mpaaeu  40891  rngunsnply  40914  idomrootle  40936  hausgraph  40953  fsovf1od  41513  brcoffn  41529  clsneiel1  41607  wfximgfd  41663  extoimad  41664  mnringmulrcld  41735  mnurndlem1  41788  caofcan  41830  ofmul12  41832  ofdivrec  41833  ofdivcan4  41834  ofdivdiv2  41835  dvconstbi  41841  binomcxplemnotnn0  41863  refsum2cnlem1  42469  ssmapsn  42645  preimaiocmnf  42989  fsumsupp0  43009  fsumsermpt  43010  climinf  43037  climinf2lem  43137  limsupmnflem  43151  limsupvaluz2  43169  supcnvlimsup  43171  limsupgtlem  43208  liminfvalxr  43214  liminflelimsupuz  43216  xlimconst2  43266  climxlim2  43277  icccncfext  43318  dvnprodlem1  43377  volicoff  43426  voliooicof  43427  fourierdlem25  43563  etransclem2  43667  etransclem35  43700  fge0iccico  43798  sge0tsms  43808  sge0sup  43819  sge0resrn  43832  sge0le  43835  sge0fodjrnlem  43844  sge0isum  43855  sge0seq  43874  nnfoctbdjlem  43883  meadjiunlem  43893  omeiunle  43945  hoicvr  43976  ovolval4lem1  44077  ovolval5lem3  44082  ovnovollem1  44084  ovnovollem2  44085  iinhoiicclem  44101  iunhoiioolem  44103  preimaicomnf  44136  smfresal  44209  smfsuplem1  44231  smflimsuplem2  44241  fcoreslem3  44446  fcoreslem4  44447  fcores  44448  mgmhmf1o  45229  resmgmhm2b  45242  mgmhmima  45244  mgmhmeql  45245  rnghmf1o  45349  ackvalsucsucval  45922  amgmwlem  46392