Theorem ffnd 6669

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

Syntax hints:   → wi 4   Fn wfn 6493  ⟶wf 6494

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 207  df-an 396  df-f 6502

This theorem is referenced by:  fnconstg  6728  f1fn  6737  fofn  6754  f1ofn  6781  feqmptd  6908  fssrescdmd  7079  fprb  7149  cocan1  7246  oprres  7535  off  7649  coof  7655  ofco  7656  caofref  7662  caofid0l  7664  caofid0r  7665  caofid1  7666  caofid2  7667  caofrss  7670  caoftrn  7672  fo2ndf  8071  fnwelem  8081  fnse  8083  suppsnop  8128  suppss  8144  suppssr  8145  suppssrg  8146  suppssof1  8149  suppofssd  8153  suppofss1d  8154  suppofss2d  8155  suppcoss  8157  smocdmdom  8308  elmapfn  8812  ralxpmap  8844  omxpenlem  9016  mapen  9079  f1finf1o  9183  unirnffid  9257  fdmfifsupp  9288  mapfien  9321  intrnfi  9329  marypha2  9352  ordtypelem7  9439  wemapsolem  9465  wemapso  9466  wemapso2lem  9467  unxpwdom2  9503  ixpiunwdom  9505  cantnfle  9592  cantnfp1lem2  9600  cantnfp1lem3  9601  cantnfp1  9602  oemapvali  9605  cantnflem1a  9606  cantnflem1c  9608  cantnflem3  9612  cantnf  9614  cnfcomlem  9620  cnfcom3  9625  updjudhcoinlf  9856  updjudhcoinrg  9857  fseqenlem1  9946  numacn  9971  infpwfien  9984  isf32lem2  10276  isf34lem7  10301  isf34lem6  10302  unirnfdomd  10490  ofsubeq0  12156  ofnegsub  12157  ofsubge0  12158  seqf1olem2  14004  resunimafz0  14407  wrdfn  14490  swrdvalfn  14614  pfxfn  14644  pfxid  14647  cats1un  14683  cshwfn  14763  ccatco  14797  limsupgle  15439  o1of2  15575  o1rlimmul  15581  isercolllem2  15628  isercoll  15630  isercoll2  15631  climsup  15632  fsumss  15687  ruclem11  16207  vdwlem2  16953  vdwlem6  16957  vdwlem9  16960  vdwlem12  16963  0ram  16991  ramub1lem1  16997  pwsle  17456  pwsleval  17457  pwsvscaval  17459  mrcuni  17587  mrcun  17588  invf1o  17736  funcres2c  17870  setcmon  18054  setcepi  18055  uncfcurf  18205  yoniso  18251  isacs4lem  18510  acsmapd  18520  chnso  18590  gsumval2  18654  mgmhmf1o  18668  resmgmhm2b  18681  mgmhmima  18683  mgmhmeql  18684  prdsplusgsgrpcl  18700  prdssgrpd  18701  prdsplusgcl  18736  prdsidlem  18737  prdsmndd  18738  mhmf1o  18764  resmhm2b  18790  mhmimalem  18792  mhmima  18793  mhmeql  18794  prdspjmhm  18797  pwsco1mhm  18800  pwsco2mhm  18801  gsumwmhm  18813  frmdss2  18831  grpinvf1o  18985  prdsinvlem  19025  cycsubgcl  19181  ghmrn  19204  ghmpreima  19213  ghmeql  19214  ghmnsgima  19215  ghmnsgpreima  19216  ghmeqker  19218  ghmf1o  19223  ghmqusnsglem1  19255  ghmqusnsg  19257  ghmquskerlem1  19258  ghmquskerco  19259  ghmquskerlem3  19261  ghmqusker  19262  gass  19276  cntzmhm  19316  symgextres  19400  gsmsymgrfixlem1  19402  fvcosymgeq  19404  f1omvdconj  19421  pmtrfinv  19436  symgtrinv  19447  pmtr3ncomlem1  19448  sygbasnfpfi  19487  efginvrel2  19702  efgredleme  19718  ghmplusg  19821  prdscmnd  19836  gsumval3a  19878  gsumval3eu  19879  gsumzaddlem  19896  gsumzsplit  19902  gsumpt  19937  prdsgsum  19956  dprdfcntz  19992  dprdfadd  19997  dprdfeq0  19999  dprdf11  20000  dprdlub  20003  dprdspan  20004  dprd2dlem1  20018  dmdprdpr  20026  dprdpr  20027  dpjlem  20028  ablfac1eu  20050  gsumle  20120  prdsmulrngcl  20156  prdsrngd  20157  prdsringd  20300  prdscrngd  20301  prds1  20302  pwspjmhmmgpd  20307  pwsgprod  20309  rnghmf1o  20432  rhmf1o  20470  rhmimasubrnglem  20542  rnrhmsubrg  20582  rrgsupp  20678  imadrhmcl  20774  isabvd  20789  lmodfopnelem1  20893  lcomfsupp  20897  prdsvscacl  20963  prdslmodd  20964  lmhmco  21038  lmhmplusg  21039  lmhmvsca  21040  lmhmf1o  21041  lmhmeql  21050  lspextmo  21051  rhmpreimaidl  21275  pjfo  21695  dsmmbas2  21717  dsmm0cl  21720  dsmmacl  21721  dsmmsubg  21723  dsmmlss  21724  frlmvplusgvalc  21747  frlmvscaval  21748  frlmplusgvalb  21749  frlmvscavalb  21750  frlmsslss2  21755  frlmphllem  21760  frlmphl  21761  frlmssuvc2  21775  frlmsslsp  21776  frlmup1  21778  frlmup2  21779  frlmup3  21780  frlmup4  21781  islindf4  21818  psrbagfsupp  21899  psrbaglesupp  21902  psrbaglecl  21903  psrbagaddcl  21904  psrbagcon  21905  psrbaglefi  21906  psrbagleadd1  21908  psrbagconf1o  21909  gsumbagdiaglem  21910  psrass1lem  21912  psrvscaval  21929  psrlidm  21940  psrridm  21941  psrass1  21942  psrdi  21943  psrdir  21944  psrascl  21957  mvrf2  21971  mplsubglem  21977  mplvscaval  21994  subrgmvrf  22012  mplbas2  22020  mplind  22048  psrbagev1  22055  psrbagev2  22056  evlslem3  22058  evlslem1  22060  evlsvvval  22071  evlsvar  22073  evladdval  22081  evlmulval  22082  mpfind  22093  ismhp3  22108  mhpmulcl  22115  psdmplcl  22128  psdadd  22129  psdvsca  22130  psdmul  22132  psdmvr  22135  psrplusgpropd  22199  coe1add  22229  coe1addfv  22230  evl1addd  22306  evl1subd  22307  evl1muld  22308  pf1mpf  22317  pf1ind  22320  evls1fpws  22334  ressply1evl  22335  rhmply1vsca  22353  mamudir  22369  mamulid  22406  mamurid  22407  mdetrlin  22567  mdetrsca  22568  mdetralt  22573  mdetunilem7  22583  mdetunilem9  22585  madurid  22609  cnrest2  23251  lmss  23263  lmcnp  23269  cnt0  23311  cnt1  23315  cnhaus  23319  rncmp  23361  conncn  23391  2ndcomap  23423  1stccnp  23427  comppfsc  23497  1stckgenlem  23518  ptbasfi  23546  ptopn  23548  ptclsg  23580  ptcnp  23587  upxp  23588  txtube  23605  txcmplem1  23606  hauseqlcld  23611  xkohaus  23618  xkoptsub  23619  cnmpt11  23628  cnmpt21  23636  cnmpt22f  23640  cnmptcom  23643  qtopss  23680  qtopeu  23681  qtopomap  23683  qtopcmap  23684  kqffn  23690  hmeof1o2  23728  xkocnv  23779  rnelfm  23918  ptcmplem1  24017  cnextfres1  24033  ghmcnp  24080  tgphaus  24082  prdstmdd  24089  prdstgpd  24090  fmucnd  24256  psmetxrge0  24278  isxmet2d  24292  prdsmet  24335  blelrnps  24381  blelrn  24382  xmetresbl  24402  comet  24478  stdbdxmet  24480  met2ndci  24487  prdsxmslem2  24494  isngp3  24563  nmotri  24704  metdsre  24819  bndth  24925  evth  24926  fmcfil  25239  bcthlem4  25294  rrxcph  25359  rrxds  25360  rrxmet  25375  evthicc2  25427  ovolfsf  25438  ovolmge0  25444  ovollb2lem  25455  ovolunlem1a  25463  ovoliunlem1  25469  ovoliun  25472  ovoliun2  25473  ovolscalem1  25480  ovolicc1  25483  ovolicc2lem4  25487  ovolicc2  25489  voliunlem1  25517  voliunlem3  25519  volsup  25523  ioombl1lem2  25526  ioombl1lem4  25528  uniiccdif  25545  uniioombllem2  25550  uniioombllem3  25552  uniioombllem6  25555  volsup2  25572  vitalilem4  25578  mbfeqalem1  25608  mbfmulc2lem  25614  mbfmax  25616  mbfaddlem  25627  mbfadd  25628  mbfsub  25629  mbfsup  25631  mbfinf  25632  itg1ge0  25653  itg1addlem1  25659  i1faddlem  25660  i1fmullem  25661  i1fadd  25662  i1fmul  25663  itg1addlem4  25666  i1fmulclem  25669  i1fmulc  25670  itg1mulc  25671  i1fres  25672  itg10a  25677  itg1ge0a  25678  itg1lea  25679  mbfi1fseqlem3  25684  mbfi1fseqlem4  25685  mbfi1flimlem  25689  mbfmullem2  25691  mbfmul  25693  itg20  25704  itg2lea  25711  itg2splitlem  25715  itg2split  25716  itg2monolem1  25717  itg2monolem2  25718  itg2monolem3  25719  itg2mono  25720  itg2i1fseqle  25721  itg2i1fseq  25722  itg2addlem  25725  itg2gt0  25727  itg2cnlem1  25728  itg2cnlem2  25729  itg2cn  25730  itgitg1  25776  bddmulibl  25806  bddibl  25807  dvidlem  25882  dvaddbr  25905  dvmulbr  25906  dvaddf  25909  dvcmulf  25912  dvrec  25922  dvcnvlem  25943  rolle  25957  dveq0  25967  dv11cn  25968  dvivthlem2  25976  dvivth  25977  dvne0  25978  lhop1lem  25980  lhop1  25981  lhop2  25982  lhop  25983  ftc1cn  26010  tdeglem1  26023  tdeglem3  26024  tdeglem4  26025  mdegleb  26029  mdegldg  26031  mdegaddle  26039  ply1remlem  26130  ply1rem  26131  fta1glem1  26133  fta1glem2  26134  fta1blem  26136  idomrootle  26138  plyeq0lem  26175  plyeq0  26176  plyaddlem1  26178  coeeulem  26189  coeaddlem  26214  coemulc  26220  dgradd2  26233  dgrcolem2  26239  ofmulrt  26248  plyrem  26271  vieta1lem1  26276  vieta1  26278  plyexmo  26279  elqaalem3  26287  aannenlem1  26294  aalioulem2  26299  ulmuni  26357  ulmdvlem1  26365  ulmdv  26368  mbfulm  26371  iblulm  26372  itgulm  26373  rlimcnp2  26930  jensen  26952  amgm  26954  basellem3  27046  basellem7  27050  basellem9  27052  dchrelbas2  27200  dchrmulcl  27212  dchrfi  27218  dchreq  27221  dchrresb  27222  dchrinv  27224  dchr1re  27226  sumdchr2  27233  dchr2sum  27236  lgsqrlem2  27310  lgsqrlem3  27311  rpvmasum2  27475  dchrisum0re  27476  mirf1o  28737  lmif1o  28863  eqeefv  28972  axlowdimlem14  29024  vtxdgfisf  29545  2pthon3v  30011  nvinvfval  30711  sspg  30799  ssps  30801  sspmlem  30803  sspn  30807  lnon0  30869  ubthlem1  30941  pjfn  31780  kbpj  32027  kbass2  32188  elpjrn  32261  ofrn2  32713  off2  32714  ofresid  32715  xppreima2  32724  ofpreima2  32739  suppovss  32754  resf1o  32803  prodindf  32922  indpreima  32925  swrdrn3  33015  pwrssmgc  33060  mgcf1o  33063  gsumfs2d  33122  gsumhashmul  33128  symgcom2  33145  pmtrcnel  33150  pmtrcnel2  33151  pmtrcnelor  33152  cycpmfvlem  33173  cycpmfv3  33176  cycpmcl  33177  cycpmco2rn  33186  cycpmco2  33194  cycpm3cl2  33197  cyc3co2  33201  cyc3evpm  33211  elrgspnlem1  33303  elrgspnlem2  33304  elrgspnlem4  33306  elrgspnsubrunlem1  33308  elrgspnsubrunlem2  33309  gsumind  33405  islinds5  33427  ellspds  33428  elrspunidl  33488  elrspunsn  33489  rhmimaidl  33492  rhmpreimaprmidl  33511  rprmdvdsprod  33594  1arithidomlem2  33596  evls1fn  33620  ply1dg1rt  33640  ply1mulrtss  33642  ply1degltel  33654  ply1degleel  33655  ply1degltlss  33656  ply1gsumz  33659  ig1pmindeg  33662  r1pquslmic  33671  extvfvcl  33680  mplmulmvr  33683  evlextv  33686  mplvrpmmhm  33690  mplvrpmrhm  33691  psrmonprod  33696  esplyfval0  33708  esplyfval2  33709  esplyfv1  33713  esplyfv  33714  esplyfval3  33716  esplyfvaln  33718  esplyind  33719  vieta  33724  exsslsb  33741  ply1degltdimlem  33766  ply1degltdim  33767  dimkerim  33771  fedgmullem2  33774  fedgmul  33775  lvecendof1f1o  33777  fldextrspunlsplem  33817  fldextrspunlsp  33818  irngss  33831  irngnzply1  33835  extdgfialglem2  33837  irngnminplynz  33856  2sqr3minply  33924  cos9thpiminply  33932  cmpcref  33994  rhmpreimacnlem  34028  fsumcvg4  34094  pl1cn  34099  qqhval2lem  34125  esumcvg  34230  ofcf  34247  ofcof  34251  measfn  34348  meascnbl  34363  sibfof  34484  sitgaddlemb  34492  subiwrdlen  34530  rrvfn  34589  plymul02  34690  signsplypnf  34694  signsply0  34695  reprsuc  34759  reprdifc  34771  breprexplema  34774  circlemethhgt  34787  hgt750lemb  34800  f1resrcmplf1dlem  35229  pthhashvtx  35310  cvmopnlem  35460  cvmliftmolem1  35463  cvmliftlem10  35476  cvmlift2lem9a  35485  cvmlift2lem6  35490  cvmlift2lem12  35496  cvmliftphtlem  35499  cvmlift3lem9  35509  mrsubrn  35695  elmrsubrn  35702  elmsubrn  35710  msubrn  35711  mclsind  35752  mclsppslem  35765  mclspps  35766  iprodefisumlem  35922  weiunfrlem  36646  mh-inf3f1  36723  matunitlindflem1  37937  poimirlem1  37942  poimirlem2  37943  poimirlem3  37944  poimirlem16  37957  poimirlem17  37958  poimirlem19  37960  poimirlem20  37961  poimirlem22  37963  poimirlem23  37964  poimirlem29  37970  poimirlem30  37971  poimirlem31  37972  poimir  37974  mblfinlem2  37979  itg2addnclem3  37994  itg2addnc  37995  itg2gt0cn  37996  ftc1cnnc  38013  ftc1anclem5  38018  ftc1anclem7  38020  ftc1anc  38022  sdclem2  38063  istotbnd3  38092  sstotbnd2  38095  isbnd3  38105  heibor1lem  38130  rrnmet  38150  grpokerinj  38214  isdrngo2  38279  lfl1  39516  lfladdcl  39517  lflvscl  39523  lkr0f  39540  lkrsc  39543  eqlkr2  39546  eqlkr3  39547  ldualvaddval  39577  ldualvsval  39584  tendoeq1  41210  zndvdchrrhm  42412  hashscontpow  42561  aks6d1c3  42562  aks6d1c2lem4  42566  aks6d1c2  42569  sticksstones1  42585  sticksstones2  42586  sticksstones3  42587  sticksstones12a  42596  sticksstones12  42597  aks6d1c6lem2  42610  aks6d1c6lem3  42611  aks6d1c6isolem1  42613  aks6d1c6isolem3  42615  aks6d1c6lem5  42616  aks6d1c7lem1  42619  unitscyglem1  42634  dvun  42791  frlmvscadiccat  42951  fiabv  42981  frlmsnic  42985  mplmapghm  42997  evlsaddval  43004  evlsmulval  43005  selvvvval  43018  evlselvlem  43019  evlselv  43020  fsuppssind  43026  mhphf  43030  ismrcd1  43130  ismrcd2  43131  istopclsd  43132  isnacs3  43142  mzpaddmpt  43173  mzpmulmpt  43174  mzpsubst  43180  mzpcong  43400  fnwe2lem2  43479  islmodfg  43497  kercvrlsm  43511  dgrsub2  43563  mpaaeu  43578  rngunsnply  43597  hausgraph  43633  ofoafg  43782  ofoafo  43784  ofoaid1  43786  ofoaid2  43787  naddcnff  43790  naddcnffn  43791  naddcnffo  43792  naddcnfcom  43794  naddcnfid1  43795  naddcnfass  43797  fsovf1od  44443  brcoffn  44457  clsneiel1  44535  wfximgfd  44590  extoimad  44591  mnringmulrcld  44655  mnurndlem1  44708  caofcan  44750  ofmul12  44752  ofdivrec  44753  ofdivcan4  44754  ofdivdiv2  44755  dvconstbi  44761  binomcxplemnotnn0  44783  relpmin  45379  refsum2cnlem1  45468  ssmapsn  45645  preimaiocmnf  45990  fsumsupp0  46008  fsumsermpt  46009  climinf  46036  climinf2lem  46134  limsupmnflem  46148  limsupvaluz2  46166  supcnvlimsup  46168  limsupgtlem  46205  liminfvalxr  46211  liminflelimsupuz  46213  xlimconst2  46263  climxlim2  46274  icccncfext  46315  dvnprodlem1  46374  volicoff  46423  voliooicof  46424  fourierdlem25  46560  etransclem2  46664  etransclem35  46697  fge0iccico  46798  sge0tsms  46808  sge0sup  46819  sge0resrn  46832  sge0le  46835  sge0fodjrnlem  46844  sge0isum  46855  sge0seq  46874  nnfoctbdjlem  46883  meadjiunlem  46893  omeiunle  46945  hoicvr  46976  ovolval4lem1  47077  ovolval5lem3  47082  ovnovollem1  47084  ovnovollem2  47085  iinhoiicclem  47101  iunhoiioolem  47103  preimaicomnf  47139  smfresal  47216  smfsuplem1  47239  smflimsuplem2  47249  fcoreslem3  47513  fcoreslem4  47514  fcores  47515  isubgredg  48342  upgrimpths  48385  ackvalsucsucval  49164  funchomf  49572  imasubc  49626  imassc  49628  imaid  49629  prcofdiag1  49868  prcofdiag  49869  oppfdiag1  49889  oppfdiag  49891  amgmwlem  50277