Theorem ffnd 6686

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

Syntax hints:   → wi 4   Fn wfn 6510  ⟶wf 6511

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 209  df-an 400  df-f 6519

This theorem is referenced by:  fnconstg  6746  f1fn  6755  fofn  6774  f1ofn  6801  feqmptd  6929  fssrescdmd  7102  fprb  7172  cocan1  7269  oprres  7558  off  7672  coof  7678  ofco  7679  caofref  7685  caofid0l  7687  caofid0r  7688  caofid1  7689  caofid2  7690  caofrss  7693  caoftrn  7695  fo2ndf  8093  fnwelem  8104  fnse  8106  suppsnop  8151  suppss  8167  suppssr  8168  suppssrg  8169  suppssof1  8172  suppofssd  8176  suppofss1d  8177  suppofss2d  8178  suppcoss  8180  smocdmdom  8332  elmapfn  8839  ralxpmap  8871  omxpenlem  9043  mapen  9106  f1finf1o  9210  unirnffid  9283  fdmfifsupp  9314  mapfien  9347  intrnfi  9355  marypha2  9378  ordtypelem7  9465  wemapsolem  9491  wemapso  9492  wemapso2lem  9493  unxpwdom2  9529  ixpiunwdom  9531  cantnfle  9619  cantnfp1lem2  9627  cantnfp1lem3  9628  cantnfp1  9629  oemapvali  9632  cantnflem1a  9633  cantnflem1c  9635  cantnflem3  9639  cantnf  9641  cnfcomlem  9647  cnfcom3  9652  updjudhcoinlf  9883  updjudhcoinrg  9884  fseqenlem1  9973  numacn  9998  infpwfien  10011  isf32lem2  10304  isf34lem7  10329  isf34lem6  10330  unirnfdomd  10518  ofsubeq0  12185  ofnegsub  12186  ofsubge0  12187  seqf1olem2  14048  resunimafz0  14451  wrdfn  14534  swrdvalfn  14658  pfxfn  14688  pfxid  14691  cats1un  14727  cshwfn  14807  ccatco  14841  limsupgle  15494  o1of2  15630  o1rlimmul  15636  isercolllem2  15683  isercoll  15685  isercoll2  15686  climsup  15687  fsumss  15742  ruclem11  16262  vdwlem2  17008  vdwlem6  17012  vdwlem9  17015  vdwlem12  17018  0ram  17046  ramub1lem1  17052  pwsle  17512  pwsleval  17513  pwsvscaval  17515  mrcuni  17643  mrcun  17644  invf1o  17792  funcres2c  17926  setcmon  18110  setcepi  18111  uncfcurf  18261  yoniso  18307  isacs4lem  18566  acsmapd  18576  chnso  18646  gsumval2  18710  mgmhmf1o  18724  resmgmhm2b  18737  mgmhmima  18739  mgmhmeql  18740  prdsplusgsgrpcl  18756  prdssgrpd  18757  prdsplusgcl  18792  prdsidlem  18793  prdsmndd  18794  mhmf1o  18820  resmhm2b  18846  mhmimalem  18848  mhmima  18849  mhmeql  18850  prdspjmhm  18853  pwsco1mhm  18856  pwsco2mhm  18857  gsumwmhm  18869  frmdss2  18887  grpinvf1o  19041  prdsinvlem  19081  cycsubgcl  19237  ghmrn  19259  ghmpreima  19268  ghmeql  19269  ghmnsgima  19270  ghmnsgpreima  19271  ghmeqker  19273  ghmf1o  19278  ghmqusnsglem1  19310  ghmqusnsg  19312  ghmquskerlem1  19313  ghmquskerco  19314  ghmquskerlem3  19316  ghmqusker  19317  gass  19331  cntzmhm  19371  symgextres  19455  gsmsymgrfixlem1  19457  fvcosymgeq  19459  f1omvdconj  19476  pmtrfinv  19491  symgtrinv  19502  pmtr3ncomlem1  19503  sygbasnfpfi  19542  efginvrel2  19757  efgredleme  19773  ghmplusg  19876  prdscmnd  19891  gsumval3a  19933  gsumval3eu  19934  gsumzaddlem  19951  gsumzsplit  19957  gsumpt  19992  prdsgsum  20011  dprdfcntz  20047  dprdfadd  20052  dprdfeq0  20054  dprdf11  20055  dprdlub  20058  dprdspan  20059  dprd2dlem1  20073  dmdprdpr  20081  dprdpr  20082  dpjlem  20083  ablfac1eu  20105  gsumle  20175  prdsmulrngcl  20211  prdsrngd  20212  prdsringd  20355  prdscrngd  20356  prds1  20357  pwspjmhmmgpd  20362  pwsgprod  20364  rnghmf1o  20487  rhmf1o  20526  rhmimasubrnglem  20601  rnrhmsubrg  20641  rrgsupp  20737  imadrhmcl  20833  isabvd  20848  lmodfopnelem1  20952  lcomfsupp  20956  prdsvscacl  21022  prdslmodd  21023  lmhmco  21097  lmhmplusg  21098  lmhmvsca  21099  lmhmf1o  21100  lmhmeql  21109  lspextmo  21110  rhmpreimaidl  21334  pjfo  21754  dsmmbas2  21776  dsmm0cl  21779  dsmmacl  21780  dsmmsubg  21782  dsmmlss  21783  frlmvplusgvalc  21806  frlmvscaval  21807  frlmplusgvalb  21808  frlmvscavalb  21809  frlmsslss2  21814  frlmphllem  21819  frlmphl  21820  frlmssuvc2  21834  frlmsslsp  21835  frlmup1  21837  frlmup2  21838  frlmup3  21839  frlmup4  21840  islindf4  21877  psrbagfsupp  21958  psrbaglesupp  21961  psrbaglecl  21962  psrbagaddcl  21963  psrbagcon  21964  psrbaglefi  21965  psrbagleadd1  21967  psrbagconf1o  21968  gsumbagdiaglem  21970  psrass1lem  21972  psrvscaval  21989  psrlidm  22000  psrridm  22001  psrass1  22002  psrdi  22003  psrdir  22004  psrascl  22017  mvrf2  22031  mplsubglem  22037  mplvscaval  22054  subrgmvrf  22074  mplbas2  22082  mplind  22110  psrbagev1  22117  psrbagev2  22118  evlslem3  22120  evlslem1  22122  evlsvvval  22133  evlsvar  22135  evladdval  22143  evlmulval  22144  mpfind  22155  mplmapghm  22162  evlsaddval  22169  evlsmulval  22170  selvvvval  22182  ismhp3  22194  mhpmulcl  22201  psdmplcl  22214  psdadd  22215  psdvsca  22216  psdmul  22218  psdmvr  22221  psrplusgpropd  22284  coe1add  22314  coe1addfv  22315  evl1addd  22391  evl1subd  22392  evl1muld  22393  pf1mpf  22402  pf1ind  22405  evls1fpws  22419  ressply1evl  22420  rhmply1vsca  22435  mamudir  22451  mamulid  22488  mamurid  22489  mdetrlin  22649  mdetrsca  22650  mdetralt  22655  mdetunilem7  22665  mdetunilem9  22667  madurid  22691  cnrest2  23333  lmss  23345  lmcnp  23351  cnt0  23393  cnt1  23397  cnhaus  23401  rncmp  23443  conncn  23473  2ndcomap  23505  1stccnp  23509  comppfsc  23579  1stckgenlem  23600  ptbasfi  23628  ptopn  23630  ptclsg  23662  ptcnp  23669  upxp  23670  txtube  23687  txcmplem1  23688  hauseqlcld  23693  xkohaus  23700  xkoptsub  23701  cnmpt11  23710  cnmpt21  23718  cnmpt22f  23722  cnmptcom  23725  qtopss  23762  qtopeu  23763  qtopomap  23765  qtopcmap  23766  kqffn  23772  hmeof1o2  23810  xkocnv  23861  rnelfm  24000  ptcmplem1  24099  cnextfres1  24115  ghmcnp  24162  tgphaus  24164  prdstmdd  24171  prdstgpd  24172  fmucnd  24338  psmetxrge0  24360  isxmet2d  24374  prdsmet  24417  blelrnps  24463  blelrn  24464  xmetresbl  24484  comet  24560  stdbdxmet  24562  met2ndci  24569  prdsxmslem2  24576  isngp3  24645  nmotri  24786  metdsre  24901  bndth  25007  evth  25008  fmcfil  25321  bcthlem4  25376  rrxcph  25441  rrxds  25442  rrxmet  25457  evthicc2  25509  ovolfsf  25520  ovolmge0  25526  ovollb2lem  25537  ovolunlem1a  25545  ovoliunlem1  25551  ovoliun  25554  ovoliun2  25555  ovolscalem1  25562  ovolicc1  25565  ovolicc2lem4  25569  ovolicc2  25571  voliunlem1  25599  voliunlem3  25601  volsup  25605  ioombl1lem2  25608  ioombl1lem4  25610  uniiccdif  25627  uniioombllem2  25632  uniioombllem3  25634  uniioombllem6  25637  volsup2  25654  vitalilem4  25660  mbfeqalem1  25690  mbfmulc2lem  25696  mbfmax  25698  mbfaddlem  25709  mbfadd  25710  mbfsub  25711  mbfsup  25713  mbfinf  25714  itg1ge0  25735  itg1addlem1  25741  i1faddlem  25742  i1fmullem  25743  i1fadd  25744  i1fmul  25745  itg1addlem4  25748  i1fmulclem  25751  i1fmulc  25752  itg1mulc  25753  i1fres  25754  itg10a  25759  itg1ge0a  25760  itg1lea  25761  mbfi1fseqlem3  25766  mbfi1fseqlem4  25767  mbfi1flimlem  25771  mbfmullem2  25773  mbfmul  25775  itg20  25786  itg2lea  25793  itg2splitlem  25797  itg2split  25798  itg2monolem1  25799  itg2monolem2  25800  itg2monolem3  25801  itg2mono  25802  itg2i1fseqle  25803  itg2i1fseq  25804  itg2addlem  25807  itg2gt0  25809  itg2cnlem1  25810  itg2cnlem2  25811  itg2cn  25812  itgitg1  25858  bddmulibl  25888  bddibl  25889  dvidlem  25964  dvaddbr  25987  dvmulbr  25988  dvaddf  25991  dvcmulf  25994  dvrec  26004  dvcnvlem  26025  rolle  26039  dveq0  26049  dv11cn  26050  dvivthlem2  26058  dvivth  26059  dvne0  26060  lhop1lem  26062  lhop1  26063  lhop2  26064  lhop  26065  ftc1cn  26092  tdeglem1  26105  tdeglem3  26106  tdeglem4  26107  mdegleb  26111  mdegldg  26113  mdegaddle  26121  ply1remlem  26212  ply1rem  26213  fta1glem1  26215  fta1glem2  26216  fta1blem  26218  idomrootle  26220  plyeq0lem  26257  plyeq0  26258  plyaddlem1  26260  coeeulem  26271  coeaddlem  26296  coemulc  26302  dgradd2  26315  dgrcolem2  26321  ofmulrt  26330  plymul02  26331  plyrem  26356  vieta1lem1  26361  vieta1  26363  plyexmo  26364  elqaalem3  26372  aannenlem1  26379  aalioulem2  26384  ulmuni  26442  ulmdvlem1  26450  ulmdv  26453  mbfulm  26456  iblulm  26457  itgulm  26458  rlimcnp2  27018  jensen  27040  amgm  27042  basellem3  27134  basellem7  27138  basellem9  27140  dchrelbas2  27288  dchrmulcl  27300  dchrfi  27306  dchreq  27309  dchrresb  27310  dchrinv  27312  dchr1re  27314  sumdchr2  27321  dchr2sum  27324  lgsqrlem2  27398  lgsqrlem3  27399  rpvmasum2  27563  dchrisum0re  27564  mirf1o  28825  lmif1o  28951  eqeefv  29060  axlowdimlem14  29112  vtxdgfisf  29633  2pthon3v  30099  nvinvfval  30799  sspg  30887  ssps  30889  sspmlem  30891  sspn  30895  lnon0  30957  ubthlem1  31029  pjfn  31868  kbpj  32115  kbass2  32276  elpjrn  32349  ofrn2  32802  off2  32803  ofresid  32804  xppreima2  32813  ofpreima2  32828  suppovss  32843  resf1o  32892  prodindf  33000  indpreima  33003  swrdrn3  33093  pwrssmgc  33138  mgcf1o  33141  gsumfs2d  33201  gsumhashmul  33207  symgcom2  33224  pmtrcnel  33229  pmtrcnel2  33230  pmtrcnelor  33231  cycpmfvlem  33252  cycpmfv3  33255  cycpmcl  33256  cycpmco2rn  33265  cycpmco2  33273  cycpm3cl2  33276  cyc3co2  33280  cyc3evpm  33290  elrgspnlem1  33383  elrgspnlem2  33384  elrgspnlem4  33386  elrgspnsubrunlem1  33388  elrgspnsubrunlem2  33389  gsumind  33491  islinds5  33513  ellspds  33514  elrspunidl  33574  elrspunsn  33575  rhmimaidl  33578  rhmpreimaprmidl  33598  rprmdvdsprod  33690  1arithidomlem2  33692  evls1fn  33716  ply1dg1rt  33736  ply1mulrtss  33738  ply1degltel  33750  ply1degleel  33751  ply1degltlss  33752  ply1gsumz  33755  ig1pmindeg  33758  r1pquslmic  33767  0mplrim  33771  mplasclco  33773  selvply1rhmlema  33775  selvply1rhmlemb  33776  selvply1rhmlem1  33777  selvply1rhmlem4  33780  selvply1rhm0  33783  extvfvcl  33793  mplmulmvr  33796  evlextv  33799  mplvrpmmhm  33803  mplvrpmrhm  33804  psrmonprod  33809  esplyfval0  33821  esplyfval2  33822  esplyfv1  33826  esplyfv  33827  esplyfval3  33829  esplyfvaln  33831  esplyind  33832  vieta  33837  exsslsb  33854  ply1degltdimlem  33879  ply1degltdim  33880  dimkerim  33884  fedgmullem2  33887  fedgmul  33888  lvecendof1f1o  33890  fldextrspunlsplem  33930  fldextrspunlsp  33931  irngss  33944  irngnzply1  33948  extdgfialglem2  33950  irngnminplynz  33969  2sqr3minply  34037  cos9thpiminply  34045  cmpcref  34107  rhmpreimacnlem  34141  fsumcvg4  34207  pl1cn  34212  qqhval2lem  34238  esumcvg  34343  ofcf  34360  ofcof  34364  measfn  34461  meascnbl  34476  sibfof  34597  sitgaddlemb  34605  subiwrdlen  34643  rrvfn  34702  signsplypnf  34804  signsply0  34805  reprsuc  34869  reprdifc  34881  breprexplema  34884  circlemethhgt  34897  hgt750lemb  34910  f1resrcmplf1dlem  35340  pthhashvtx  35438  cvmopnlem  35588  cvmliftmolem1  35591  cvmliftlem10  35604  cvmlift2lem9a  35613  cvmlift2lem6  35618  cvmlift2lem12  35624  cvmliftphtlem  35627  cvmlift3lem9  35637  mrsubrn  35823  elmrsubrn  35830  elmsubrn  35838  msubrn  35839  mclsind  35880  mclsppslem  35893  mclspps  35894  iprodefisumlem  36050  weiunfrlem  36784  mh-inf3f1  36861  matunitlindflem1  38075  poimirlem1  38080  poimirlem2  38081  poimirlem3  38082  poimirlem16  38095  poimirlem17  38096  poimirlem19  38098  poimirlem20  38099  poimirlem22  38101  poimirlem23  38102  poimirlem29  38108  poimirlem30  38109  poimirlem31  38110  poimir  38112  mblfinlem2  38117  itg2addnclem3  38132  itg2addnc  38133  itg2gt0cn  38134  ftc1cnnc  38151  ftc1anclem5  38156  ftc1anclem7  38158  ftc1anc  38160  sdclem2  38201  istotbnd3  38230  sstotbnd2  38233  isbnd3  38243  heibor1lem  38268  rrnmet  38288  grpokerinj  38352  isdrngo2  38417  lfl1  39654  lfladdcl  39655  lflvscl  39661  lkr0f  39678  lkrsc  39681  eqlkr2  39684  eqlkr3  39685  ldualvaddval  39715  ldualvsval  39722  tendoeq1  41348  zndvdchrrhm  42550  hashscontpow  42699  aks6d1c3  42700  aks6d1c2lem4  42704  aks6d1c2  42707  sticksstones1  42723  sticksstones2  42724  sticksstones3  42725  sticksstones12a  42734  sticksstones12  42735  aks6d1c6lem2  42748  aks6d1c6lem3  42749  aks6d1c6isolem1  42751  aks6d1c6isolem3  42753  aks6d1c6lem5  42754  aks6d1c7lem1  42757  unitscyglem1  42772  dvun  42928  frlmvscadiccat  43088  fiabv  43114  frlmsnic  43118  evlselvlem  43130  evlselv  43131  fsuppssind  43135  mhphf  43139  ismrcd1  43239  ismrcd2  43240  istopclsd  43241  isnacs3  43251  mzpaddmpt  43282  mzpmulmpt  43283  mzpsubst  43289  mzpcong  43509  fnwe2lem2  43588  islmodfg  43606  kercvrlsm  43620  dgrsub2  43672  mpaaeu  43687  rngunsnply  43706  hausgraph  43742  ofoafg  43891  ofoafo  43893  ofoaid1  43895  ofoaid2  43896  naddcnff  43899  naddcnffn  43900  naddcnffo  43901  naddcnfcom  43903  naddcnfid1  43904  naddcnfass  43906  fsovf1od  44552  brcoffn  44566  clsneiel1  44644  wfximgfd  44699  extoimad  44700  mnringmulrcld  44764  mnurndlem1  44817  caofcan  44859  ofmul12  44861  ofdivrec  44862  ofdivcan4  44863  ofdivdiv2  44864  dvconstbi  44870  binomcxplemnotnn0  44892  relpmin  45488  refsum2cnlem1  45577  ssmapsn  45752  preimaiocmnf  46096  fsumsupp0  46114  fsumsermpt  46115  climinf  46142  climinf2lem  46240  limsupmnflem  46254  limsupvaluz2  46272  supcnvlimsup  46274  limsupgtlem  46311  liminfvalxr  46317  liminflelimsupuz  46319  xlimconst2  46369  climxlim2  46380  icccncfext  46421  dvnprodlem1  46480  volicoff  46529  voliooicof  46530  fourierdlem25  46666  fourierdlem48  46688  fourierdlem49  46689  etransclem2  46770  etransclem35  46803  fge0iccico  46904  sge0tsms  46914  sge0sup  46925  sge0resrn  46938  sge0le  46941  sge0fodjrnlem  46950  sge0isum  46961  sge0seq  46980  nnfoctbdjlem  46989  meadjiunlem  46999  omeiunle  47051  hoicvr  47082  ovolval4lem1  47183  ovolval5lem3  47188  ovnovollem1  47190  ovnovollem2  47191  iinhoiicclem  47207  iunhoiioolem  47209  preimaicomnf  47245  smfresal  47322  smfsuplem1  47345  smflimsuplem2  47355  fcoreslem3  47619  fcoreslem4  47620  fcores  47621  isubgredg  48448  upgrimpths  48491  ackvalsucsucval  49270  funchomf  49678  imasubc  49732  imassc  49734  imaid  49735  prcofdiag1  49974  prcofdiag  49975  oppfdiag1  49995  oppfdiag  49997  amgmwlem  50383