Theorem ffnd 6711

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

This proof depends on syntax axioms:   → wi 4   Fn wfn 6534  ⟶wf 6535

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-f 6543

This theorem is used by:  fnconstg  6771  f1fn  6780  fofn  6799  f1ofn  6826  feqmptd  6954  fssrescdmd  7128  fprb  7200  f1resrcmplf1dlem  7279  cocan1  7300  oprres  7589  off  7712  coof  7718  ofco  7719  caofref  7725  caofid0l  7727  caofid0r  7728  caofid1  7729  caofid2  7730  caofrss  7733  caoftrn  7735  fo2ndf  8135  fnwelem  8146  fnwe2lem3  8150  fnse  8153  suppsnop  8199  suppss  8215  suppssr  8216  suppssrg  8217  suppssof1  8220  suppofssd  8224  suppofss1d  8225  suppofss2d  8226  suppcoss  8228  smocdmdom  8380  elmapfn  8891  ralxpmap  8928  omxpenlem  9101  mapen  9164  f1finf1o  9268  unirnffid  9340  fdmfifsupp  9371  mapfien  9404  intrnfi  9412  marypha2  9435  ordtypelem7  9522  wemapsolem  9548  wemapso  9549  wemapso2lem  9550  unxpwdom2  9586  ixpiunwdom  9588  cantnfle  9676  cantnfp1lem2  9684  cantnfp1lem3  9685  cantnfp1  9686  oemapvali  9689  cantnflem1a  9690  cantnflem1c  9692  cantnflem3  9696  cantnf  9698  cnfcomlem  9704  cnfcom3  9709  updjudhcoinlf  10017  updjudhcoinrg  10018  fseqenlem1  10107  numacn  10132  infpwfien  10145  isf32lem2  10436  isf34lem7  10461  isf34lem6  10462  unirnfdomd  10656  ofsubeq0  12321  ofnegsub  12322  ofsubge0  12323  seqf1olem2  14189  resunimafz0  14594  wrdfn  14677  swrdvalfn  14805  swrdrn3  14807  pfxfn  14836  pfxid  14839  cats1un  14875  cshwfn  14957  ccatco  14991  limsupgle  15650  o1of2  15786  o1rlimmul  15792  isercolllem2  15839  isercoll  15841  isercoll2  15842  climsup  15843  fsumss  15897  ruclem11  16414  vdwlem2  17166  vdwlem6  17170  vdwlem9  17173  vdwlem12  17176  0ram  17204  ramub1lem1  17210  pwsle  17670  pwsleval  17671  pwsvscaval  17673  mrcuni  17801  mrcun  17802  invf1o  17950  funcres2c  18084  setcmon  18268  setcepi  18269  uncfcurf  18419  yoniso  18465  isacs4lem  18724  acsmapd  18734  chnso  18804  mgmn0plusgplusf  18834  gsumval2  18881  mgmhmf1o  18895  resmgmhm2b  18908  mgmhmima  18910  mgmhmeql  18911  prdsplusgsgrpcl  18927  prdssgrpd  18928  prdsplusgcl  18968  prdsidlem  18969  prdsmndd  18970  mhmf1o  18997  resmhm2b  19024  mhmimalem  19026  mhmima  19027  mhmeql  19028  prdspjmhm  19031  pwsco1mhm  19034  pwsco2mhm  19035  gsumwmhm  19047  frmdss2  19065  grpinvf1o  19225  prdsinvlem  19265  cycsubgcl  19427  ghmrn  19449  ghmpreima  19458  ghmeql  19459  ghmnsgima  19460  ghmnsgpreima  19461  ghmeqker  19463  ghmf1o  19468  ghmqusnsglem1  19500  ghmqusnsg  19502  ghmquskerlem1  19503  ghmquskerco  19504  ghmquskerlem3  19506  ghmqusker  19507  gass  19521  cntzmhm  19561  symgextres  19645  gsmsymgrfixlem1  19647  fvcosymgeq  19649  f1omvdconj  19666  pmtrfinv  19681  symgtrinv  19692  pmtr3ncomlem1  19693  sygbasnfpfi  19732  efginvrel2  19947  efgredleme  19963  ghmplusg  20066  prdscmnd  20081  gsumval3a  20123  gsumval3eu  20124  gsumzaddlem  20141  gsumzsplit  20147  gsumpt  20182  prdsgsum  20201  dprdfcntz  20237  dprdfadd  20242  dprdfeq0  20244  dprdf11  20245  dprdlub  20248  dprdspan  20249  dprd2dlem1  20263  dmdprdpr  20271  dprdpr  20272  dpjlem  20273  ablfac1eu  20295  gsumle  20365  prdsmulrngcl  20403  prdsrngd  20404  prdsringd  20556  prdscrngd  20557  prds1  20558  pwspjmhmmgpd  20563  pwsgprod  20565  rnghmf1o  20688  rhmf1o  20733  rhmimasubrnglem  20823  rnrhmsubrg  20863  rrgsupp  20959  imadrhmcl  21060  isabvd  21075  lmodfopnelem1  21179  lcomfsupp  21183  prdsvscacl  21249  prdslmodd  21250  lmhmco  21324  lmhmplusg  21325  lmhmvsca  21326  lmhmf1o  21327  lmhmeql  21336  lspextmo  21337  rhmpreimaidl  21577  rhmpreimaprmidl  21641  pjfo  22027  dsmmbas2  22049  dsmm0cl  22052  dsmmacl  22053  dsmmsubg  22055  dsmmlss  22056  frlmvplusgvalc  22079  frlmvscaval  22080  frlmplusgvalb  22081  frlmvscavalb  22082  frlmsslss2  22087  frlmphllem  22092  frlmphl  22093  frlmssuvc2  22107  frlmsslsp  22108  frlmup1  22110  frlmup2  22111  frlmup3  22112  frlmup4  22113  islindf4  22150  psrbagfsupp  22233  psrbaglesupp  22236  psrbaglecl  22237  psrbagaddcl  22238  psrbagcon  22239  psrbaglefi  22240  psrbagleadd1  22242  psrbagconf1o  22243  gsumbagdiaglem  22245  psrass1lem  22247  psrvscaval  22264  psrlidm  22275  psrridm  22276  psrass1  22277  psrdi  22278  psrdir  22279  psrascl  22292  mvrf2  22306  mplsubglem  22312  mplvscaval  22329  subrgmvrf  22349  mplbas2  22357  mplind  22385  psrbagev1  22392  psrbagev2  22393  evlslem3  22395  evlslem1  22397  evlsvvval  22408  evlsvar  22410  evladdval  22418  evlmulval  22419  mpfind  22430  mplmapghm  22437  evlsaddval  22444  evlsmulval  22445  selvvvval  22457  ismhp3  22469  mhpmulcl  22476  psdmplcl  22489  psdadd  22490  psdvsca  22491  psdmul  22493  psdmvr  22496  psrplusgpropd  22559  coe1add  22589  coe1addfv  22590  evl1addd  22665  evl1subd  22666  evl1muld  22667  pf1mpf  22676  pf1ind  22679  evls1fpws  22693  ressply1evl  22694  rhmply1vsca  22709  mamudir  22725  mamulid  22762  mamurid  22763  mdetrlin  22923  mdetrsca  22924  mdetralt  22929  mdetunilem7  22939  mdetunilem9  22941  madurid  22965  matunitlindflem1  23000  cnrest2  23610  lmss  23622  lmcnp  23628  cnt0  23670  cnt1  23674  cnhaus  23678  rncmp  23720  conncn  23750  2ndcomap  23783  1stccnp  23787  comppfsc  23857  1stckgenlem  23878  ptbasfi  23906  ptopn  23908  ptclsg  23940  ptcnp  23947  upxp  23948  txtube  23965  txcmplem1  23966  hauseqlcld  23971  xkohaus  23978  xkoptsub  23979  cnmpt11  23988  cnmpt21  23996  cnmpt22f  24000  cnmptcom  24003  qtopss  24040  qtopeu  24041  qtopomap  24043  qtopcmap  24044  kqffn  24050  hmeof1o2  24088  xkocnv  24139  rnelfm  24278  ptcmplem1  24377  cnextfres1  24393  ghmcnp  24440  tgphaus  24442  prdstmdd  24449  prdstgpd  24450  fmucnd  24616  psmetxrge0  24638  isxmet2d  24652  prdsmet  24695  blelrnps  24741  blelrn  24742  xmetresbl  24762  comet  24838  stdbdxmet  24840  met2ndci  24847  prdsxmslem2  24854  isngp3  24923  nmotri  25064  metdsre  25179  bndth  25285  evth  25286  fmcfil  25599  bcthlem4  25654  rrxcph  25719  rrxds  25720  rrxmet  25735  evthicc2  25787  ovolfsf  25798  ovolmge0  25804  ovollb2lem  25815  ovolunlem1a  25823  ovoliunlem1  25829  ovoliun  25832  ovoliun2  25833  ovolscalem1  25840  ovolicc1  25843  ovolicc2lem4  25847  ovolicc2  25849  voliunlem1  25877  voliunlem3  25879  volsup  25883  ioombl1lem2  25886  ioombl1lem4  25888  uniiccdif  25905  uniioombllem2  25910  uniioombllem3  25912  uniioombllem6  25915  volsup2  25932  vitalilem4  25938  mbfeqalem1  25968  mbfmulc2lem  25974  mbfmax  25976  mbfaddlem  25987  mbfadd  25988  mbfsub  25989  mbfsup  25991  mbfinf  25992  itg1ge0  26013  itg1addlem1  26019  i1faddlem  26020  i1fmullem  26021  i1fadd  26022  i1fmul  26023  itg1addlem4  26026  i1fmulclem  26029  i1fmulc  26030  itg1mulc  26031  i1fres  26032  itg10a  26037  itg1ge0a  26038  itg1lea  26039  mbfi1fseqlem3  26044  mbfi1fseqlem4  26045  mbfi1flimlem  26049  mbfmullem2  26051  mbfmul  26053  itg20  26064  itg2lea  26071  itg2splitlem  26075  itg2split  26076  itg2monolem1  26077  itg2monolem2  26078  itg2monolem3  26079  itg2mono  26080  itg2i1fseqle  26081  itg2i1fseq  26082  itg2addlem  26085  itg2gt0  26087  itg2cnlem1  26088  itg2cnlem2  26089  itg2cn  26090  itgitg1  26135  bddmulibl  26165  bddibl  26166  dvidlem  26241  dvaddbr  26264  dvmulbr  26265  dvaddf  26268  dvcmulf  26271  dvrec  26281  dvcnvlem  26302  rolle  26316  dveq0  26326  dv11cn  26327  dvivthlem2  26335  dvivth  26336  dvne0  26337  lhop1lem  26339  lhop1  26340  lhop2  26341  lhop  26342  ftc1cn  26369  tdeglem1  26382  tdeglem3  26383  tdeglem4  26384  mdegleb  26388  mdegldg  26390  mdegaddle  26398  ply1remlem  26489  ply1rem  26490  fta1glem1  26492  fta1glem2  26493  fta1blem  26495  idomrootle  26497  plyeq0lem  26535  plyeq0  26536  plyaddlem1  26538  coeeulem  26549  coeaddlem  26574  coemulc  26580  dgradd2  26593  dgrcolem2  26599  ofmulrt  26606  plymul02  26607  plyrem  26632  rnplynfin  26636  plyconz  26637  vieta1lem1  26639  vieta1  26641  plyexmo  26642  elqaalem3  26650  aannenlem1  26661  aalioulem2  26666  ulmuni  26725  ulmdvlem1  26733  ulmdv  26736  mbfulm  26739  iblulm  26740  itgulm  26741  rlimcnp2  27300  jensen  27322  amgm  27324  basellem3  27416  basellem7  27420  basellem9  27422  dchrelbas2  27570  dchrmulcl  27582  dchrfi  27588  dchreq  27591  dchrresb  27592  dchrinv  27594  dchr1re  27596  sumdchr2  27603  dchr2sum  27606  lgsqrlem2  27680  lgsqrlem3  27681  rpvmasum2  27845  dchrisum0re  27846  mirf1o  29147  lmif1o  29306  elcgrabasi  29381  eqeefv  29487  axlowdimlem14  29539  vtxdgfisf  30063  pthhashvtx  30321  2pthon3v  30538  nvinvfval  31248  sspg  31336  ssps  31338  sspmlem  31340  sspn  31344  lnon0  31406  ubthlem1  31478  pjfn  32317  kbpj  32564  kbass2  32725  elpjrn  32798  ofrn2  33282  off2  33283  ofresid  33284  xppreima2  33293  ofpreima2  33308  suppovss  33322  resf1o  33369  prodindf  33476  indpreima  33479  pwrssmgc  33608  mgcf1o  33611  gsumfs2d  33669  gsumhashmul  33675  symgcom2  33692  pmtrcnel  33697  pmtrcnel2  33698  pmtrcnelor  33699  cycpmfvlem  33720  cycpmfv3  33723  cycpmcl  33724  cycpmco2rn  33733  cycpmco2  33741  cycpm3cl2  33744  cyc3co2  33748  cyc3evpm  33758  elrgspnlem1  33850  elrgspnlem2  33851  elrgspnlem4  33853  elrgspnsubrunlem1  33855  elrgspnsubrunlem2  33856  gsumind  33953  islinds5  33970  ellspds  33971  elrspunidl  34025  elrspunsn  34026  rhmimaidl  34029  rprmdvdsprod  34113  1arithidomlem2  34115  evls1fn  34139  ply1dg1rt  34159  ply1mulrtss  34161  ply1degltel  34173  ply1degleel  34174  ply1degltlss  34175  ply1gsumz  34178  ig1pmindeg  34181  r1pquslmic  34189  0mplrim  34193  mplasclco  34195  selvply1rhmlema  34197  selvply1rhmlemb  34198  selvply1rhmlem1  34199  selvply1rhmlem4  34202  selvply1rhm0  34205  extvfvcl  34215  mplmulmvr  34218  evlextv  34221  mplvrpmmhm  34225  mplvrpmrhm  34226  psrmonprod  34231  esplyfval0  34243  esplyfval2  34244  esplyfv1  34248  esplyfv  34249  esplyfval3  34251  esplyfvaln  34253  esplyind  34254  vieta  34259  exsslsb  34276  ply1degltdimlem  34301  ply1degltdim  34302  dimkerim  34306  fedgmullem2  34309  fedgmul  34310  lvecendof1f1o  34312  fldextrspunlsplem  34352  fldextrspunlsp  34353  irngss  34366  irngnzply1  34370  extdgfialglem2  34372  irngnminplynz  34391  2sqr3minply  34459  cos9thpiminply  34467  cmpcref  34529  rhmpreimacnlem  34563  fsumcvg4  34629  pl1cn  34634  qqhval2lem  34660  esumcvg  34765  ofcf  34782  ofcof  34786  measfn  34884  meascnbl  34899  sibfof  35019  sitgaddlemb  35027  subiwrdlen  35065  rrvfn  35124  signsplypnf  35226  signsply0  35227  reprsuc  35291  reprdifc  35303  breprexplema  35306  circlemethhgt  35319  hgt750lemb  35332  onprcf1acwevd  35967  cvmopnlem  36130  cvmliftmolem1  36133  cvmliftlem10  36146  cvmlift2lem9a  36155  cvmlift2lem6  36160  cvmlift2lem12  36166  cvmliftphtlem  36169  cvmlift3lem9  36179  mrsubrn  36365  elmrsubrn  36372  elmsubrn  36380  msubrn  36381  mclsind  36422  mclsppslem  36435  mclspps  36436  iprodefisumlem  36598  weiunfrlem  37345  mh-inf3f1  37422  poimirlem1  38633  poimirlem2  38634  poimirlem3  38635  poimirlem16  38648  poimirlem17  38649  poimirlem19  38651  poimirlem20  38652  poimirlem22  38654  poimirlem23  38655  poimirlem29  38661  poimirlem30  38662  poimirlem31  38663  poimir  38665  mblfinlem2  38670  itg2addnclem3  38685  itg2addnc  38686  itg2gt0cn  38687  ftc1cnnc  38704  ftc1anclem5  38709  ftc1anclem7  38711  ftc1anc  38713  sdclem2  38770  istotbnd3  38799  sstotbnd2  38802  isbnd3  38812  heibor1lem  38837  rrnmet  38857  grpokerinj  38921  isdrngo2  38986  lfl1  40221  lfladdcl  40222  lflvscl  40228  lkr0f  40245  lkrsc  40248  eqlkr2  40251  eqlkr3  40252  ldualvaddval  40282  ldualvsval  40289  tendoeq1  41915  zndvdchrrhm  43117  hashscontpow  43266  aks6d1c3  43267  aks6d1c2lem4  43271  aks6d1c2  43274  sticksstones1  43290  sticksstones2  43291  sticksstones3  43292  sticksstones12a  43301  sticksstones12  43302  aks6d1c6lem2  43315  aks6d1c6lem3  43316  aks6d1c6isolem1  43318  aks6d1c6isolem3  43320  aks6d1c6lem5  43321  aks6d1c7lem1  43324  unitscyglem1  43339  dvun  43504  frlmbasfn  43659  frlmvscadiccat  43667  fiabv  43694  frlmsnic  43698  evlselvlem  43710  evlselv  43711  fsuppssind  43715  mhphf  43719  ismrcd1  43803  ismrcd2  43804  istopclsd  43805  isnacs3  43815  mzpaddmpt  43846  mzpmulmpt  43847  mzpsubst  43853  mzpcong  44073  islmodfg  44165  kercvrlsm  44179  dgrsub2  44231  mpaaeu  44246  rngunsnply  44265  hausgraph  44301  ofoafg  44450  ofoafo  44452  ofoaid1  44454  ofoaid2  44455  naddcnff  44458  naddcnffn  44459  naddcnffo  44460  naddcnfcom  44462  naddcnfid1  44463  naddcnfass  44465  fsovf1od  45110  brcoffn  45124  clsneiel1  45202  wfximgfd  45257  extoimad  45258  mnringmulrcld  45320  mnurndlem1  45359  caofcan  45401  ofmul12  45403  ofdivrec  45404  ofdivcan4  45405  ofdivdiv2  45406  dvconstbi  45412  binomcxplemnotnn0  45434  relpmin  46036  refsum2cnlem1  46148  ssmapsn  46323  preimaiocmnf  46666  fsumsupp0  46684  fsumsermpt  46685  climinf  46712  climinf2lem  46810  limsupmnflem  46824  limsupvaluz2  46842  supcnvlimsup  46844  limsupgtlem  46881  liminfvalxr  46887  liminflelimsupuz  46889  xlimconst2  46939  climxlim2  46950  icccncfext  46991  dvnprodlem1  47050  volicoff  47099  voliooicof  47100  fourierdlem25  47236  fourierdlem48  47258  fourierdlem49  47259  etransclem2  47340  etransclem35  47373  fge0iccico  47474  sge0tsms  47484  sge0sup  47495  sge0resrn  47508  sge0le  47511  sge0fodjrnlem  47520  sge0isum  47531  sge0seq  47550  nnfoctbdjlem  47559  meadjiunlem  47569  omeiunle  47621  hoicvr  47652  ovolval4lem1  47753  ovolval5lem3  47758  ovnovollem1  47760  ovnovollem2  47761  iinhoiicclem  47777  iunhoiioolem  47779  preimaicomnf  47815  smfresal  47892  smfsuplem1  47915  smflimsuplem2  47925  tmachlem-franscan  48053  fcoreslem3  48229  fcoreslem4  48230  fcores  48231  isubgredg  49058  upgrimpths  49101  ackvalsucsucval  49894  funchomf  50307  imasubc  50361  imassc  50363  imaid  50364  prcofdiag1  50622  prcofdiag  50623  oppfdiag1  50643  oppfdiag  50645  crossp3d  51136  veroquadmodzerod  51153  amgmwlem  51156