Theorem ffnd 6706

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

Syntax hints:   → wi 4   Fn wfn 6525  ⟶wf 6526

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 6534

This theorem is referenced by:  fnconstg  6765  f1fn  6774  fofn  6791  f1ofn  6818  feqmptd  6946  fssrescdmd  7115  fprb  7185  cocan1  7283  oprres  7573  off  7687  coof  7693  ofco  7694  caofref  7700  caofid0l  7702  caofid0r  7703  caofid1  7704  caofid2  7705  caofrss  7708  caoftrn  7710  fo2ndf  8118  fnwelem  8128  fnse  8130  suppsnop  8175  suppss  8191  suppssr  8192  suppssrg  8193  suppssof1  8196  suppofssd  8200  suppofss1d  8201  suppofss2d  8202  suppcoss  8204  smocdmdom  8380  elmapfn  8877  ralxpmap  8908  omxpenlem  9085  mapen  9153  f1finf1o  9275  f1finf1oOLD  9276  unirnffid  9357  fdmfifsupp  9385  mapfien  9418  intrnfi  9426  marypha2  9449  ordtypelem7  9536  wemapsolem  9562  wemapso  9563  wemapso2lem  9564  unxpwdom2  9600  ixpiunwdom  9602  cantnfle  9683  cantnfp1lem2  9691  cantnfp1lem3  9692  cantnfp1  9693  oemapvali  9696  cantnflem1a  9697  cantnflem1c  9699  cantnflem3  9703  cantnf  9705  cnfcomlem  9711  cnfcom3  9716  updjudhcoinlf  9944  updjudhcoinrg  9945  fseqenlem1  10036  numacn  10061  infpwfien  10074  isf32lem2  10366  isf34lem7  10391  isf34lem6  10392  unirnfdomd  10579  ofsubeq0  12235  ofnegsub  12236  ofsubge0  12237  seqf1olem2  14058  resunimafz0  14461  wrdfn  14544  swrdvalfn  14667  pfxfn  14697  pfxid  14700  cats1un  14737  cshwfn  14817  ccatco  14852  limsupgle  15491  o1of2  15627  o1rlimmul  15633  isercolllem2  15680  isercoll  15682  isercoll2  15683  climsup  15684  fsumss  15739  ruclem11  16256  vdwlem2  17000  vdwlem6  17004  vdwlem9  17007  vdwlem12  17010  0ram  17038  ramub1lem1  17044  pwsle  17504  pwsleval  17505  pwsvscaval  17507  mrcuni  17631  mrcun  17632  invf1o  17780  funcres2c  17914  setcmon  18098  setcepi  18099  uncfcurf  18249  yoniso  18295  isacs4lem  18552  acsmapd  18562  gsumval2  18662  mgmhmf1o  18676  resmgmhm2b  18689  mgmhmima  18691  mgmhmeql  18692  prdsplusgsgrpcl  18708  prdssgrpd  18709  prdsplusgcl  18744  prdsidlem  18745  prdsmndd  18746  mhmf1o  18772  resmhm2b  18798  mhmimalem  18800  mhmima  18801  mhmeql  18802  prdspjmhm  18805  pwsco1mhm  18808  pwsco2mhm  18809  gsumwmhm  18821  frmdss2  18839  grpinvf1o  18990  prdsinvlem  19030  cycsubgcl  19187  ghmrn  19210  ghmpreima  19219  ghmeql  19220  ghmnsgima  19221  ghmnsgpreima  19222  ghmeqker  19224  ghmf1o  19229  ghmqusnsglem1  19261  ghmqusnsg  19263  ghmquskerlem1  19264  ghmquskerco  19265  ghmquskerlem3  19267  ghmqusker  19268  gass  19282  cntzmhm  19322  symgextres  19404  gsmsymgrfixlem1  19406  fvcosymgeq  19408  f1omvdconj  19425  pmtrfinv  19440  symgtrinv  19451  pmtr3ncomlem1  19452  sygbasnfpfi  19491  efginvrel2  19706  efgredleme  19722  ghmplusg  19825  prdscmnd  19840  gsumval3a  19882  gsumval3eu  19883  gsumzaddlem  19900  gsumzsplit  19906  gsumpt  19941  prdsgsum  19960  dprdfcntz  19996  dprdfadd  20001  dprdfeq0  20003  dprdf11  20004  dprdlub  20007  dprdspan  20008  dprd2dlem1  20022  dmdprdpr  20030  dprdpr  20031  dpjlem  20032  ablfac1eu  20054  prdsmulrngcl  20133  prdsrngd  20134  prdsringd  20279  prdscrngd  20280  prds1  20281  pwspjmhmmgpd  20286  rnghmf1o  20410  rhmf1o  20449  rhmimasubrnglem  20523  rnrhmsubrg  20563  rrgsupp  20659  imadrhmcl  20755  isabvd  20770  lmodfopnelem1  20853  lcomfsupp  20857  prdsvscacl  20923  prdslmodd  20924  lmhmco  20999  lmhmplusg  21000  lmhmvsca  21001  lmhmf1o  21002  lmhmeql  21011  lspextmo  21012  rhmpreimaidl  21236  pjfo  21673  dsmmbas2  21695  dsmm0cl  21698  dsmmacl  21699  dsmmsubg  21701  dsmmlss  21702  frlmvplusgvalc  21725  frlmvscaval  21726  frlmplusgvalb  21727  frlmvscavalb  21728  frlmsslss2  21733  frlmphllem  21738  frlmphl  21739  frlmssuvc2  21753  frlmsslsp  21754  frlmup1  21756  frlmup2  21757  frlmup3  21758  frlmup4  21759  islindf4  21796  psrbagfsupp  21877  psrbaglesupp  21880  psrbaglecl  21881  psrbagaddcl  21882  psrbagcon  21883  psrbaglefi  21884  psrbagleadd1  21886  psrbagconf1o  21887  gsumbagdiaglem  21888  psrass1lem  21890  psrvscaval  21908  psrlidm  21920  psrridm  21921  psrass1  21922  psrdi  21923  psrdir  21924  psrascl  21937  mvrf2  21951  mplsubglem  21957  mplvscaval  21974  subrgmvrf  21990  mplbas2  21998  mplind  22026  psrbagev1  22033  psrbagev2  22034  evlslem3  22036  evlslem1  22038  evlsvar  22046  mpfind  22063  ismhp3  22078  mhpmulcl  22085  psdmplcl  22098  psdadd  22099  psdvsca  22100  psdmul  22102  psdmvr  22105  psrplusgpropd  22169  coe1add  22199  coe1addfv  22200  evl1addd  22277  evl1subd  22278  evl1muld  22279  pf1mpf  22288  pf1ind  22291  evls1fpws  22305  ressply1evl  22306  rhmply1vsca  22324  mamudir  22340  mamulid  22377  mamurid  22378  mdetrlin  22538  mdetrsca  22539  mdetralt  22544  mdetunilem7  22554  mdetunilem9  22556  madurid  22580  cnrest2  23222  lmss  23234  lmcnp  23240  cnt0  23282  cnt1  23286  cnhaus  23290  rncmp  23332  conncn  23362  2ndcomap  23394  1stccnp  23398  comppfsc  23468  1stckgenlem  23489  ptbasfi  23517  ptopn  23519  ptclsg  23551  ptcnp  23558  upxp  23559  txtube  23576  txcmplem1  23577  hauseqlcld  23582  xkohaus  23589  xkoptsub  23590  cnmpt11  23599  cnmpt21  23607  cnmpt22f  23611  cnmptcom  23614  qtopss  23651  qtopeu  23652  qtopomap  23654  qtopcmap  23655  kqffn  23661  hmeof1o2  23699  xkocnv  23750  rnelfm  23889  ptcmplem1  23988  cnextfres1  24004  ghmcnp  24051  tgphaus  24053  prdstmdd  24060  prdstgpd  24061  fmucnd  24228  psmetxrge0  24250  isxmet2d  24264  prdsmet  24307  blelrnps  24353  blelrn  24354  xmetresbl  24374  comet  24450  stdbdxmet  24452  met2ndci  24459  prdsxmslem2  24466  isngp3  24535  nmotri  24676  metdsre  24791  bndth  24906  evth  24907  fmcfil  25222  bcthlem4  25277  rrxcph  25342  rrxds  25343  rrxmet  25358  evthicc2  25411  ovolfsf  25422  ovolmge0  25428  ovollb2lem  25439  ovolunlem1a  25447  ovoliunlem1  25453  ovoliun  25456  ovoliun2  25457  ovolscalem1  25464  ovolicc1  25467  ovolicc2lem4  25471  ovolicc2  25473  voliunlem1  25501  voliunlem3  25503  volsup  25507  ioombl1lem2  25510  ioombl1lem4  25512  uniiccdif  25529  uniioombllem2  25534  uniioombllem3  25536  uniioombllem6  25539  volsup2  25556  vitalilem4  25562  mbfeqalem1  25592  mbfmulc2lem  25598  mbfmax  25600  mbfaddlem  25611  mbfadd  25612  mbfsub  25613  mbfsup  25615  mbfinf  25616  itg1ge0  25637  itg1addlem1  25643  i1faddlem  25644  i1fmullem  25645  i1fadd  25646  i1fmul  25647  itg1addlem4  25650  i1fmulclem  25653  i1fmulc  25654  itg1mulc  25655  i1fres  25656  itg10a  25661  itg1ge0a  25662  itg1lea  25663  mbfi1fseqlem3  25668  mbfi1fseqlem4  25669  mbfi1flimlem  25673  mbfmullem2  25675  mbfmul  25677  itg20  25688  itg2lea  25695  itg2splitlem  25699  itg2split  25700  itg2monolem1  25701  itg2monolem2  25702  itg2monolem3  25703  itg2mono  25704  itg2i1fseqle  25705  itg2i1fseq  25706  itg2addlem  25709  itg2gt0  25711  itg2cnlem1  25712  itg2cnlem2  25713  itg2cn  25714  itgitg1  25760  bddmulibl  25790  bddibl  25791  dvidlem  25866  dvaddbr  25890  dvmulbr  25891  dvmulbrOLD  25892  dvaddf  25895  dvcmulf  25898  dvrec  25909  dvcnvlem  25930  rolle  25944  dveq0  25955  dv11cn  25956  dvivthlem2  25964  dvivth  25965  dvne0  25966  lhop1lem  25968  lhop1  25969  lhop2  25970  lhop  25971  ftc1cn  26000  tdeglem1  26013  tdeglem3  26014  tdeglem4  26015  mdegleb  26019  mdegldg  26021  mdegaddle  26029  ply1remlem  26120  ply1rem  26121  fta1glem1  26123  fta1glem2  26124  fta1blem  26126  idomrootle  26128  plyeq0lem  26165  plyeq0  26166  plyaddlem1  26168  coeeulem  26179  coeaddlem  26204  coemulc  26210  dgradd2  26224  dgrcolem2  26230  ofmulrt  26239  plyrem  26263  vieta1lem1  26268  vieta1  26270  plyexmo  26271  elqaalem3  26279  aannenlem1  26286  aalioulem2  26291  ulmuni  26351  ulmdvlem1  26359  ulmdv  26362  mbfulm  26365  iblulm  26366  itgulm  26367  rlimcnp2  26926  jensen  26949  amgm  26951  basellem3  27043  basellem7  27047  basellem9  27049  dchrelbas2  27198  dchrmulcl  27210  dchrfi  27216  dchreq  27219  dchrresb  27220  dchrinv  27222  dchr1re  27224  sumdchr2  27231  dchr2sum  27234  lgsqrlem2  27308  lgsqrlem3  27309  rpvmasum2  27473  dchrisum0re  27474  mirf1o  28594  lmif1o  28720  eqeefv  28828  axlowdimlem14  28880  vtxdgfisf  29402  2pthon3v  29871  nvinvfval  30567  sspg  30655  ssps  30657  sspmlem  30659  sspn  30663  lnon0  30725  ubthlem1  30797  pjfn  31636  kbpj  31883  kbass2  32044  elpjrn  32117  ofrn2  32564  off2  32565  ofresid  32566  xppreima2  32575  ofpreima2  32590  suppovss  32604  resf1o  32653  prodindf  32786  indpreima  32788  swrdrn3  32877  pwrssmgc  32926  mgcf1o  32929  chnso  32940  gsumfs2d  32995  gsumhashmul  33001  gsumle  33038  symgcom2  33041  pmtrcnel  33046  pmtrcnel2  33047  pmtrcnelor  33048  cycpmfvlem  33069  cycpmfv3  33072  cycpmcl  33073  cycpmco2rn  33082  cycpmco2  33090  cycpm3cl2  33093  cyc3co2  33097  cyc3evpm  33107  elrgspnlem1  33183  elrgspnlem2  33184  elrgspnlem4  33186  elrgspnsubrunlem1  33188  elrgspnsubrunlem2  33189  islinds5  33328  ellspds  33329  elrspunidl  33389  elrspunsn  33390  rhmimaidl  33393  rhmpreimaprmidl  33412  rprmdvdsprod  33495  1arithidomlem2  33497  evls1fn  33519  ply1dg1rt  33538  ply1mulrtss  33540  ply1degltel  33550  ply1degleel  33551  ply1degltlss  33552  ply1gsumz  33554  ig1pmindeg  33557  r1pquslmic  33566  exsslsb  33582  ply1degltdimlem  33608  ply1degltdim  33609  dimkerim  33613  fedgmullem2  33616  fedgmul  33617  lvecendof1f1o  33619  fldextrspunlsplem  33660  fldextrspunlsp  33661  irngss  33674  irngnzply1  33678  irngnminplynz  33692  2sqr3minply  33760  cos9thpiminply  33768  cmpcref  33827  rhmpreimacnlem  33861  fsumcvg4  33927  pl1cn  33932  qqhval2lem  33958  esumcvg  34063  ofcf  34080  ofcof  34084  measfn  34181  meascnbl  34196  sibfof  34318  sitgaddlemb  34326  subiwrdlen  34364  rrvfn  34423  plymul02  34524  signsplypnf  34528  signsply0  34529  reprsuc  34593  reprdifc  34605  breprexplema  34608  circlemethhgt  34621  hgt750lemb  34634  f1resrcmplf1dlem  35063  pthhashvtx  35096  cvmopnlem  35246  cvmliftmolem1  35249  cvmliftlem10  35262  cvmlift2lem9a  35271  cvmlift2lem6  35276  cvmlift2lem12  35282  cvmliftphtlem  35285  cvmlift3lem9  35295  mrsubrn  35481  elmrsubrn  35488  elmsubrn  35496  msubrn  35497  mclsind  35538  mclsppslem  35551  mclspps  35552  iprodefisumlem  35703  weiunfrlem  36428  matunitlindflem1  37586  poimirlem1  37591  poimirlem2  37592  poimirlem3  37593  poimirlem16  37606  poimirlem17  37607  poimirlem19  37609  poimirlem20  37610  poimirlem22  37612  poimirlem23  37613  poimirlem29  37619  poimirlem30  37620  poimirlem31  37621  poimir  37623  mblfinlem2  37628  itg2addnclem3  37643  itg2addnc  37644  itg2gt0cn  37645  ftc1cnnc  37662  ftc1anclem5  37667  ftc1anclem7  37669  ftc1anc  37671  sdclem2  37712  istotbnd3  37741  sstotbnd2  37744  isbnd3  37754  heibor1lem  37779  rrnmet  37799  grpokerinj  37863  isdrngo2  37928  lfl1  39034  lfladdcl  39035  lflvscl  39041  lkr0f  39058  lkrsc  39061  eqlkr2  39064  eqlkr3  39065  ldualvaddval  39095  ldualvsval  39102  tendoeq1  40729  zndvdchrrhm  41931  hashscontpow  42081  aks6d1c3  42082  aks6d1c2lem4  42086  aks6d1c2  42089  sticksstones1  42105  sticksstones2  42106  sticksstones3  42107  sticksstones12a  42116  sticksstones12  42117  aks6d1c6lem2  42130  aks6d1c6lem3  42131  aks6d1c6isolem1  42133  aks6d1c6isolem3  42135  aks6d1c6lem5  42136  aks6d1c7lem1  42139  unitscyglem1  42154  metakunt19  42182  metakunt25  42188  metakunt33  42196  dvun  42349  frlmvscadiccat  42476  fiabv  42506  frlmsnic  42510  pwsgprod  42514  mplmapghm  42526  evlsvvval  42533  evlsaddval  42538  evlsmulval  42539  evladdval  42545  evlmulval  42546  selvvvval  42555  evlselvlem  42556  evlselv  42557  fsuppssind  42563  mhphf  42567  ismrcd1  42668  ismrcd2  42669  istopclsd  42670  isnacs3  42680  mzpaddmpt  42711  mzpmulmpt  42712  mzpsubst  42718  mzpcong  42943  fnwe2lem2  43022  islmodfg  43040  kercvrlsm  43054  dgrsub2  43106  mpaaeu  43121  rngunsnply  43140  hausgraph  43176  ofoafg  43325  ofoafo  43327  ofoaid1  43329  ofoaid2  43330  naddcnff  43333  naddcnffn  43334  naddcnffo  43335  naddcnfcom  43337  naddcnfid1  43338  naddcnfass  43340  fsovf1od  43987  brcoffn  44001  clsneiel1  44079  wfximgfd  44134  extoimad  44135  mnringmulrcld  44200  mnurndlem1  44253  caofcan  44295  ofmul12  44297  ofdivrec  44298  ofdivcan4  44299  ofdivdiv2  44300  dvconstbi  44306  binomcxplemnotnn0  44328  relpmin  44925  refsum2cnlem1  45009  ssmapsn  45188  preimaiocmnf  45537  fsumsupp0  45555  fsumsermpt  45556  climinf  45583  climinf2lem  45683  limsupmnflem  45697  limsupvaluz2  45715  supcnvlimsup  45717  limsupgtlem  45754  liminfvalxr  45760  liminflelimsupuz  45762  xlimconst2  45812  climxlim2  45823  icccncfext  45864  dvnprodlem1  45923  volicoff  45972  voliooicof  45973  fourierdlem25  46109  etransclem2  46213  etransclem35  46246  fge0iccico  46347  sge0tsms  46357  sge0sup  46368  sge0resrn  46381  sge0le  46384  sge0fodjrnlem  46393  sge0isum  46404  sge0seq  46423  nnfoctbdjlem  46432  meadjiunlem  46442  omeiunle  46494  hoicvr  46525  ovolval4lem1  46626  ovolval5lem3  46631  ovnovollem1  46633  ovnovollem2  46634  iinhoiicclem  46650  iunhoiioolem  46652  preimaicomnf  46688  smfresal  46765  smfsuplem1  46788  smflimsuplem2  46798  fcoreslem3  47042  fcoreslem4  47043  fcores  47044  isubgredg  47827  upgrimpths  47870  ackvalsucsucval  48616  funchomf  49005  imasubc  49039  imassc  49041  imaid  49042  amgmwlem  49614