Theorem ffnd 6488

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 6487	. 2 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴)
3	1, 2	syl 17	1 ⊢ (𝜑 → 𝐹 Fn 𝐴)

Syntax hints:   → wi 4   Fn wfn 6319  ⟶wf 6320

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 6328

This theorem is referenced by:  fnconstg  6541  f1fn  6550  fofn  6567  f1ofn  6591  feqmptd  6708  fprb  6933  rnmptcOLD  6947  cocan1  7025  oprres  7296  off  7404  ofco  7409  caofref  7415  caofid0l  7417  caofid0r  7418  caofid1  7419  caofid2  7420  caofrss  7422  caoftrn  7424  fo2ndf  7800  fnwelem  7808  fnse  7810  suppsnop  7827  suppss  7843  suppssr  7844  suppssof1  7846  suppofssd  7850  suppofss1d  7851  suppofss2d  7852  suppcoss  7854  smorndom  7988  elmapfn  8412  ralxpmap  8443  omxpenlem  8601  mapen  8665  f1finf1o  8729  unirnffid  8800  fdmfifsupp  8827  mapfien  8855  intrnfi  8864  marypha2  8887  ordtypelem7  8972  wemapsolem  8998  wemapso  8999  wemapso2lem  9000  unxpwdom2  9036  ixpiunwdom  9038  cantnfle  9118  cantnfp1lem2  9126  cantnfp1lem3  9127  cantnfp1  9128  oemapvali  9131  cantnflem1a  9132  cantnflem1c  9134  cantnflem3  9138  cantnf  9140  cnfcomlem  9146  cnfcom3  9151  updjudhcoinlf  9345  updjudhcoinrg  9346  fseqenlem1  9435  numacn  9460  infpwfien  9473  isf32lem2  9765  isf34lem7  9790  isf34lem6  9791  unirnfdomd  9978  ofsubeq0  11622  ofnegsub  11623  ofsubge0  11624  seqf1olem2  13406  resunimafz0  13799  wrdfn  13871  swrdvalfn  14004  pfxfn  14034  pfxid  14037  cats1un  14074  cshwfn  14154  ccatco  14188  limsupgle  14826  o1of2  14961  o1rlimmul  14967  isercolllem2  15014  isercoll  15016  isercoll2  15017  climsup  15018  fsumss  15074  ruclem11  15585  vdwlem2  16308  vdwlem6  16312  vdwlem9  16315  vdwlem12  16318  0ram  16346  ramub1lem1  16352  pwsle  16757  pwsleval  16758  pwsvscaval  16760  mrcuni  16884  mrcun  16885  invf1o  17031  funcres2c  17163  setcmon  17339  setcepi  17340  uncfcurf  17481  yoniso  17527  isacs4lem  17770  acsmapd  17780  gsumval2  17888  prdsplusgcl  17934  prdsidlem  17935  prdsmndd  17936  mhmf1o  17958  resmhm2b  17979  mhmima  17981  mhmeql  17982  prdspjmhm  17985  pwsco1mhm  17988  pwsco2mhm  17989  gsumwmhm  18002  frmdss2  18020  grpinvf1o  18161  prdsinvlem  18200  cycsubgcl  18341  ghmrn  18363  ghmpreima  18372  ghmeql  18373  ghmnsgima  18374  ghmnsgpreima  18375  ghmeqker  18377  ghmf1o  18380  gass  18423  cntzmhm  18461  symgextres  18545  gsmsymgrfixlem1  18547  fvcosymgeq  18549  f1omvdconj  18566  pmtrfinv  18581  symgtrinv  18592  pmtr3ncomlem1  18593  sygbasnfpfi  18632  efginvrel2  18845  efgredleme  18861  ghmplusg  18959  prdscmnd  18974  gsumval3a  19016  gsumval3eu  19017  gsumzaddlem  19034  gsumzsplit  19040  gsumpt  19075  prdsgsum  19094  dprdfcntz  19130  dprdfadd  19135  dprdfeq0  19137  dprdf11  19138  dprdlub  19141  dprdspan  19142  dprd2dlem1  19156  dmdprdpr  19164  dprdpr  19165  dpjlem  19166  ablfac1eu  19188  prdsmulrcl  19357  prdsringd  19358  prdscrngd  19359  prds1  19360  rhmf1o  19480  rnrhmsubrg  19560  isabvd  19584  lmodfopnelem1  19663  lcomfsupp  19667  prdsvscacl  19733  prdslmodd  19734  lmhmco  19808  lmhmplusg  19809  lmhmvsca  19810  lmhmf1o  19811  lmhmeql  19820  lspextmo  19821  rrgsupp  20057  pjfo  20404  dsmmbas2  20426  dsmm0cl  20429  dsmmacl  20430  dsmmsubg  20432  dsmmlss  20433  frlmvplusgvalc  20456  frlmvscaval  20457  frlmplusgvalb  20458  frlmvscavalb  20459  frlmsslss2  20464  frlmphllem  20469  frlmphl  20470  frlmssuvc2  20484  frlmsslsp  20485  frlmup1  20487  frlmup2  20488  frlmup3  20489  frlmup4  20490  islindf4  20527  psrbaglesupp  20606  psrbagcon  20609  psrbaglefi  20610  psrbagconf1o  20612  gsumbagdiaglem  20613  psrvscaval  20630  psrlidm  20641  psrridm  20642  psrass1  20643  psrdi  20644  psrdir  20645  mplsubglem  20672  mplvscaval  20687  subrgmvrf  20702  mplbas2  20710  mvrf2  20731  mplind  20741  psrbagev1  20749  evlslem3  20752  evlslem1  20754  evlsvar  20762  mpfind  20779  mhpvarcl  20798  psrplusgpropd  20865  coe1add  20893  coe1addfv  20894  evl1addd  20965  evl1subd  20966  evl1muld  20967  pf1mpf  20976  pf1ind  20979  mamudir  21009  mamulid  21046  mamurid  21047  mdetrlin  21207  mdetrsca  21208  mdetralt  21213  mdetunilem7  21223  mdetunilem9  21225  madurid  21249  cnrest2  21891  lmss  21903  lmcnp  21909  cnt0  21951  cnt1  21955  cnhaus  21959  rncmp  22001  conncn  22031  2ndcomap  22063  1stccnp  22067  comppfsc  22137  1stckgenlem  22158  ptbasfi  22186  ptopn  22188  ptclsg  22220  ptcnp  22227  upxp  22228  txtube  22245  txcmplem1  22246  hauseqlcld  22251  xkohaus  22258  xkoptsub  22259  cnmpt11  22268  cnmpt21  22276  cnmpt22f  22280  cnmptcom  22283  qtopss  22320  qtopeu  22321  qtopomap  22323  qtopcmap  22324  kqffn  22330  hmeof1o2  22368  xkocnv  22419  rnelfm  22558  ptcmplem1  22657  cnextfres1  22673  ghmcnp  22720  tgphaus  22722  prdstmdd  22729  prdstgpd  22730  fmucnd  22898  psmetxrge0  22920  isxmet2d  22934  prdsmet  22977  blelrnps  23023  blelrn  23024  xmetresbl  23044  comet  23120  stdbdxmet  23122  met2ndci  23129  prdsxmslem2  23136  isngp3  23204  nmotri  23345  metdsre  23458  bndth  23563  evth  23564  fmcfil  23876  bcthlem4  23931  rrxcph  23996  rrxds  23997  rrxmet  24012  evthicc2  24064  ovolfsf  24075  ovolmge0  24081  ovollb2lem  24092  ovolunlem1a  24100  ovoliunlem1  24106  ovoliun  24109  ovoliun2  24110  ovolscalem1  24117  ovolicc1  24120  ovolicc2lem4  24124  ovolicc2  24126  voliunlem1  24154  voliunlem3  24156  volsup  24160  ioombl1lem2  24163  ioombl1lem4  24165  uniiccdif  24182  uniioombllem2  24187  uniioombllem3  24189  uniioombllem6  24192  volsup2  24209  vitalilem4  24215  mbfeqalem1  24245  mbfmulc2lem  24251  mbfmax  24253  mbfaddlem  24264  mbfadd  24265  mbfsub  24266  mbfsup  24268  mbfinf  24269  itg1ge0  24290  itg1addlem1  24296  i1faddlem  24297  i1fmullem  24298  i1fadd  24299  i1fmul  24300  itg1addlem4  24303  i1fmulclem  24306  i1fmulc  24307  itg1mulc  24308  i1fres  24309  itg10a  24314  itg1ge0a  24315  itg1lea  24316  mbfi1fseqlem3  24321  mbfi1fseqlem4  24322  mbfi1flimlem  24326  mbfmullem2  24328  mbfmul  24330  itg20  24341  itg2lea  24348  itg2splitlem  24352  itg2split  24353  itg2monolem1  24354  itg2monolem2  24355  itg2monolem3  24356  itg2mono  24357  itg2i1fseqle  24358  itg2i1fseq  24359  itg2addlem  24362  itg2gt0  24364  itg2cnlem1  24365  itg2cnlem2  24366  itg2cn  24367  itgitg1  24412  bddmulibl  24442  bddibl  24443  dvidlem  24518  dvaddbr  24541  dvmulbr  24542  dvaddf  24545  dvcmulf  24548  dvrec  24558  dvcnvlem  24579  rolle  24593  dveq0  24603  dv11cn  24604  dvivthlem2  24612  dvivth  24613  dvne0  24614  lhop1lem  24616  lhop1  24617  lhop2  24618  lhop  24619  ftc1cn  24646  tdeglem4  24661  mdegleb  24665  mdegldg  24667  mdegaddle  24675  ply1remlem  24763  ply1rem  24764  fta1glem1  24766  fta1glem2  24767  fta1blem  24769  plyeq0lem  24807  plyeq0  24808  plyaddlem1  24810  coeeulem  24821  coeaddlem  24846  coemulc  24852  dgradd2  24865  dgrcolem2  24871  ofmulrt  24878  plyrem  24901  vieta1lem1  24906  vieta1  24908  plyexmo  24909  elqaalem3  24917  aannenlem1  24924  aalioulem2  24929  ulmuni  24987  ulmdvlem1  24995  ulmdv  24998  mbfulm  25001  iblulm  25002  itgulm  25003  rlimcnp2  25552  jensen  25574  amgm  25576  basellem3  25668  basellem7  25672  basellem9  25674  dchrelbas2  25821  dchrmulcl  25833  dchrfi  25839  dchreq  25842  dchrresb  25843  dchrinv  25845  dchr1re  25847  sumdchr2  25854  dchr2sum  25857  lgsqrlem2  25931  lgsqrlem3  25932  rpvmasum2  26096  dchrisum0re  26097  mirf1o  26463  lmif1o  26589  eqeefv  26697  axlowdimlem14  26749  vtxdgfisf  27266  2pthon3v  27729  nvinvfval  28423  sspg  28511  ssps  28513  sspmlem  28515  sspn  28519  lnon0  28581  ubthlem1  28653  pjfn  29492  kbpj  29739  kbass2  29900  elpjrn  29973  ofrn2  30401  off2  30402  ofresid  30403  xppreima2  30413  ofpreima2  30429  suppovss  30443  resf1o  30492  swrdrn3  30655  pwrssmgc  30706  gsumhashmul  30741  gsumle  30775  symgcom2  30778  pmtrcnel  30783  pmtrcnel2  30784  pmtrcnelor  30785  cycpmfvlem  30804  cycpmfv3  30807  cycpmcl  30808  cycpmco2rn  30817  cycpmco2  30825  cycpm3cl2  30828  cyc3co2  30832  cyc3evpm  30842  islinds5  30983  ellspds  30984  rhmpreimaidl  31011  elrspunidl  31014  rhmimaidl  31017  rhmpreimaprmidl  31035  dimkerim  31111  fedgmullem2  31114  fedgmul  31115  cmpcref  31203  rhmpreimacnlem  31237  fsumcvg4  31303  pl1cn  31308  qqhval2lem  31332  prodindf  31392  indpreima  31394  esumcvg  31455  ofcf  31472  ofcof  31476  measfn  31573  meascnbl  31588  sibfof  31708  sitgaddlemb  31716  subiwrdlen  31754  rrvfn  31813  plymul02  31926  signsplypnf  31930  signsply0  31931  reprsuc  31996  reprdifc  32008  breprexplema  32011  circlemethhgt  32024  hgt750lemb  32037  f1resrcmplf1dlem  32469  pthhashvtx  32487  cvmopnlem  32638  cvmliftmolem1  32641  cvmliftlem10  32654  cvmlift2lem9a  32663  cvmlift2lem6  32668  cvmlift2lem12  32674  cvmliftphtlem  32677  cvmlift3lem9  32687  mrsubrn  32873  elmrsubrn  32880  elmsubrn  32888  msubrn  32889  mclsind  32930  mclsppslem  32943  mclspps  32944  iprodefisumlem  33085  matunitlindflem1  35053  poimirlem1  35058  poimirlem2  35059  poimirlem3  35060  poimirlem16  35073  poimirlem17  35074  poimirlem19  35076  poimirlem20  35077  poimirlem22  35079  poimirlem23  35080  poimirlem29  35086  poimirlem30  35087  poimirlem31  35088  poimir  35090  mblfinlem2  35095  itg2addnclem3  35110  itg2addnc  35111  itg2gt0cn  35112  ftc1cnnc  35129  ftc1anclem5  35134  ftc1anclem7  35136  ftc1anc  35138  sdclem2  35180  istotbnd3  35209  sstotbnd2  35212  isbnd3  35222  heibor1lem  35247  rrnmet  35267  grpokerinj  35331  isdrngo2  35396  lfl1  36366  lfladdcl  36367  lflvscl  36373  lkr0f  36390  lkrsc  36393  eqlkr2  36396  eqlkr3  36397  ldualvaddval  36427  ldualvsval  36434  tendoeq1  38060  metakunt19  39368  metakunt25  39374  metakunt33  39382  frlmvscadiccat  39440  frlmsnic  39453  fsuppssind  39459  ismrcd1  39639  ismrcd2  39640  istopclsd  39641  isnacs3  39651  mzpaddmpt  39682  mzpmulmpt  39683  mzpsubst  39689  mzpcong  39913  fnwe2lem2  39995  islmodfg  40013  kercvrlsm  40027  dgrsub2  40079  mpaaeu  40094  rngunsnply  40117  idomrootle  40139  hausgraph  40156  fsovf1od  40717  brcoffn  40733  clsneiel1  40811  wfximgfd  40867  extoimad  40868  mnringmulrcld  40936  mnurndlem1  40989  caofcan  41027  ofmul12  41029  ofdivrec  41030  ofdivcan4  41031  ofdivdiv2  41032  dvconstbi  41038  binomcxplemnotnn0  41060  refsum2cnlem1  41666  ssmapsn  41845  preimaiocmnf  42198  fsumsupp0  42220  fsumsermpt  42221  climinf  42248  climinf2lem  42348  limsupmnflem  42362  limsupvaluz2  42380  supcnvlimsup  42382  limsupgtlem  42419  liminfvalxr  42425  liminflelimsupuz  42427  xlimconst2  42477  climxlim2  42488  icccncfext  42529  dvnprodlem1  42588  volicoff  42637  voliooicof  42638  fourierdlem25  42774  etransclem2  42878  etransclem35  42911  fge0iccico  43009  sge0tsms  43019  sge0sup  43030  sge0resrn  43043  sge0le  43046  sge0fodjrnlem  43055  sge0isum  43066  sge0seq  43085  nnfoctbdjlem  43094  meadjiunlem  43104  omeiunle  43156  hoicvr  43187  ovolval4lem1  43288  ovolval5lem3  43293  ovnovollem1  43295  ovnovollem2  43296  iinhoiicclem  43312  iunhoiioolem  43314  preimaicomnf  43347  smfresal  43420  smfsuplem1  43442  smflimsuplem2  43452  mgmhmf1o  44407  resmgmhm2b  44420  mgmhmima  44422  mgmhmeql  44423  rnghmf1o  44527  ackvalsucsucval  45102  amgmwlem  45330