Theorem ffnd 6719

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

Syntax hints:   → wi 4   Fn wfn 6539  ⟶wf 6540

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 206  df-an 398  df-f 6548

This theorem is referenced by:  fnconstg  6780  f1fn  6789  fofn  6808  f1ofn  6835  feqmptd  6961  fprb  7195  rnmptcOLD  7209  cocan1  7289  oprres  7575  off  7688  ofco  7693  caofref  7699  caofid0l  7701  caofid0r  7702  caofid1  7703  caofid2  7704  caofrss  7706  caoftrn  7708  fo2ndf  8107  fnwelem  8117  fnse  8119  suppsnop  8163  suppss  8179  suppssOLD  8180  suppssr  8181  suppssrg  8182  suppssof1  8184  suppofssd  8188  suppofss1d  8189  suppofss2d  8190  suppcoss  8192  smocdmdom  8368  elmapfn  8859  ralxpmap  8890  omxpenlem  9073  mapen  9141  f1finf1o  9271  f1finf1oOLD  9272  unirnffid  9344  fdmfifsupp  9373  mapfien  9403  intrnfi  9411  marypha2  9434  ordtypelem7  9519  wemapsolem  9545  wemapso  9546  wemapso2lem  9547  unxpwdom2  9583  ixpiunwdom  9585  cantnfle  9666  cantnfp1lem2  9674  cantnfp1lem3  9675  cantnfp1  9676  oemapvali  9679  cantnflem1a  9680  cantnflem1c  9682  cantnflem3  9686  cantnf  9688  cnfcomlem  9694  cnfcom3  9699  updjudhcoinlf  9927  updjudhcoinrg  9928  fseqenlem1  10019  numacn  10044  infpwfien  10057  isf32lem2  10349  isf34lem7  10374  isf34lem6  10375  unirnfdomd  10562  ofsubeq0  12209  ofnegsub  12210  ofsubge0  12211  seqf1olem2  14008  resunimafz0  14404  wrdfn  14478  swrdvalfn  14601  pfxfn  14631  pfxid  14634  cats1un  14671  cshwfn  14751  ccatco  14786  limsupgle  15421  o1of2  15557  o1rlimmul  15563  isercolllem2  15612  isercoll  15614  isercoll2  15615  climsup  15616  fsumss  15671  ruclem11  16183  vdwlem2  16915  vdwlem6  16919  vdwlem9  16922  vdwlem12  16925  0ram  16953  ramub1lem1  16959  pwsle  17438  pwsleval  17439  pwsvscaval  17441  mrcuni  17565  mrcun  17566  invf1o  17716  funcres2c  17852  setcmon  18037  setcepi  18038  uncfcurf  18192  yoniso  18238  isacs4lem  18497  acsmapd  18507  gsumval2  18605  prdsplusgsgrpcl  18623  prdssgrpd  18624  prdsplusgcl  18656  prdsidlem  18657  prdsmndd  18658  mhmf1o  18682  resmhm2b  18703  mhmimalem  18705  mhmima  18706  mhmeql  18707  prdspjmhm  18710  pwsco1mhm  18713  pwsco2mhm  18714  gsumwmhm  18726  frmdss2  18744  grpinvf1o  18893  prdsinvlem  18932  cycsubgcl  19083  ghmrn  19105  ghmpreima  19114  ghmeql  19115  ghmnsgima  19116  ghmnsgpreima  19117  ghmeqker  19119  ghmf1o  19122  gass  19165  cntzmhm  19205  symgextres  19293  gsmsymgrfixlem1  19295  fvcosymgeq  19297  f1omvdconj  19314  pmtrfinv  19329  symgtrinv  19340  pmtr3ncomlem1  19341  sygbasnfpfi  19380  efginvrel2  19595  efgredleme  19611  ghmplusg  19714  prdscmnd  19729  gsumval3a  19771  gsumval3eu  19772  gsumzaddlem  19789  gsumzsplit  19795  gsumpt  19830  prdsgsum  19849  dprdfcntz  19885  dprdfadd  19890  dprdfeq0  19892  dprdf11  19893  dprdlub  19896  dprdspan  19897  dprd2dlem1  19911  dmdprdpr  19919  dprdpr  19920  dpjlem  19921  ablfac1eu  19943  prdsmulrcl  20133  prdsringd  20134  prdscrngd  20135  prds1  20136  pwspjmhmmgpd  20141  rhmf1o  20269  rnrhmsubrg  20352  imadrhmcl  20413  isabvd  20428  lmodfopnelem1  20508  lcomfsupp  20512  prdsvscacl  20579  prdslmodd  20580  lmhmco  20654  lmhmplusg  20655  lmhmvsca  20656  lmhmf1o  20657  lmhmeql  20666  lspextmo  20667  rrgsupp  20907  pjfo  21270  dsmmbas2  21292  dsmm0cl  21295  dsmmacl  21296  dsmmsubg  21298  dsmmlss  21299  frlmvplusgvalc  21322  frlmvscaval  21323  frlmplusgvalb  21324  frlmvscavalb  21325  frlmsslss2  21330  frlmphllem  21335  frlmphl  21336  frlmssuvc2  21350  frlmsslsp  21351  frlmup1  21353  frlmup2  21354  frlmup3  21355  frlmup4  21356  islindf4  21393  psrbagfsupp  21473  psrbaglesupp  21477  psrbaglesuppOLD  21478  psrbaglecl  21479  psrbagaddcl  21481  psrbagcon  21483  psrbagconOLD  21484  psrbaglefi  21485  psrbaglefiOLD  21486  psrbagconf1o  21489  psrbagconf1oOLD  21490  gsumbagdiaglemOLD  21491  gsumbagdiaglem  21494  psrass1lem  21496  psrvscaval  21511  psrlidm  21523  psrridm  21524  psrass1  21525  psrdi  21526  psrdir  21527  mvrf2  21552  mplsubglem  21558  mplvscaval  21575  subrgmvrf  21589  mplbas2  21597  mplind  21631  psrbagev1  21638  psrbagev1OLD  21639  psrbagev2  21640  evlslem3  21643  evlslem1  21645  evlsvar  21653  mpfind  21670  ismhp3  21686  mhpmulcl  21692  psrplusgpropd  21758  coe1add  21786  coe1addfv  21787  evl1addd  21860  evl1subd  21861  evl1muld  21862  pf1mpf  21871  pf1ind  21874  mamudir  21904  mamulid  21943  mamurid  21944  mdetrlin  22104  mdetrsca  22105  mdetralt  22110  mdetunilem7  22120  mdetunilem9  22122  madurid  22146  cnrest2  22790  lmss  22802  lmcnp  22808  cnt0  22850  cnt1  22854  cnhaus  22858  rncmp  22900  conncn  22930  2ndcomap  22962  1stccnp  22966  comppfsc  23036  1stckgenlem  23057  ptbasfi  23085  ptopn  23087  ptclsg  23119  ptcnp  23126  upxp  23127  txtube  23144  txcmplem1  23145  hauseqlcld  23150  xkohaus  23157  xkoptsub  23158  cnmpt11  23167  cnmpt21  23175  cnmpt22f  23179  cnmptcom  23182  qtopss  23219  qtopeu  23220  qtopomap  23222  qtopcmap  23223  kqffn  23229  hmeof1o2  23267  xkocnv  23318  rnelfm  23457  ptcmplem1  23556  cnextfres1  23572  ghmcnp  23619  tgphaus  23621  prdstmdd  23628  prdstgpd  23629  fmucnd  23797  psmetxrge0  23819  isxmet2d  23833  prdsmet  23876  blelrnps  23922  blelrn  23923  xmetresbl  23943  comet  24022  stdbdxmet  24024  met2ndci  24031  prdsxmslem2  24038  isngp3  24107  nmotri  24256  metdsre  24369  bndth  24474  evth  24475  fmcfil  24789  bcthlem4  24844  rrxcph  24909  rrxds  24910  rrxmet  24925  evthicc2  24977  ovolfsf  24988  ovolmge0  24994  ovollb2lem  25005  ovolunlem1a  25013  ovoliunlem1  25019  ovoliun  25022  ovoliun2  25023  ovolscalem1  25030  ovolicc1  25033  ovolicc2lem4  25037  ovolicc2  25039  voliunlem1  25067  voliunlem3  25069  volsup  25073  ioombl1lem2  25076  ioombl1lem4  25078  uniiccdif  25095  uniioombllem2  25100  uniioombllem3  25102  uniioombllem6  25105  volsup2  25122  vitalilem4  25128  mbfeqalem1  25158  mbfmulc2lem  25164  mbfmax  25166  mbfaddlem  25177  mbfadd  25178  mbfsub  25179  mbfsup  25181  mbfinf  25182  itg1ge0  25203  itg1addlem1  25209  i1faddlem  25210  i1fmullem  25211  i1fadd  25212  i1fmul  25213  itg1addlem4  25216  itg1addlem4OLD  25217  i1fmulclem  25220  i1fmulc  25221  itg1mulc  25222  i1fres  25223  itg10a  25228  itg1ge0a  25229  itg1lea  25230  mbfi1fseqlem3  25235  mbfi1fseqlem4  25236  mbfi1flimlem  25240  mbfmullem2  25242  mbfmul  25244  itg20  25255  itg2lea  25262  itg2splitlem  25266  itg2split  25267  itg2monolem1  25268  itg2monolem2  25269  itg2monolem3  25270  itg2mono  25271  itg2i1fseqle  25272  itg2i1fseq  25273  itg2addlem  25276  itg2gt0  25278  itg2cnlem1  25279  itg2cnlem2  25280  itg2cn  25281  itgitg1  25326  bddmulibl  25356  bddibl  25357  dvidlem  25432  dvaddbr  25455  dvmulbr  25456  dvaddf  25459  dvcmulf  25462  dvrec  25472  dvcnvlem  25493  rolle  25507  dveq0  25517  dv11cn  25518  dvivthlem2  25526  dvivth  25527  dvne0  25528  lhop1lem  25530  lhop1  25531  lhop2  25532  lhop  25533  ftc1cn  25560  tdeglem1  25573  tdeglem3  25575  tdeglem4  25577  tdeglem4OLD  25578  mdegleb  25582  mdegldg  25584  mdegaddle  25592  ply1remlem  25680  ply1rem  25681  fta1glem1  25683  fta1glem2  25684  fta1blem  25686  plyeq0lem  25724  plyeq0  25725  plyaddlem1  25727  coeeulem  25738  coeaddlem  25763  coemulc  25769  dgradd2  25782  dgrcolem2  25788  ofmulrt  25795  plyrem  25818  vieta1lem1  25823  vieta1  25825  plyexmo  25826  elqaalem3  25834  aannenlem1  25841  aalioulem2  25846  ulmuni  25904  ulmdvlem1  25912  ulmdv  25915  mbfulm  25918  iblulm  25919  itgulm  25920  rlimcnp2  26471  jensen  26493  amgm  26495  basellem3  26587  basellem7  26591  basellem9  26593  dchrelbas2  26740  dchrmulcl  26752  dchrfi  26758  dchreq  26761  dchrresb  26762  dchrinv  26764  dchr1re  26766  sumdchr2  26773  dchr2sum  26776  lgsqrlem2  26850  lgsqrlem3  26851  rpvmasum2  27015  dchrisum0re  27016  mirf1o  27920  lmif1o  28046  eqeefv  28161  axlowdimlem14  28213  vtxdgfisf  28733  2pthon3v  29197  nvinvfval  29893  sspg  29981  ssps  29983  sspmlem  29985  sspn  29989  lnon0  30051  ubthlem1  30123  pjfn  30962  kbpj  31209  kbass2  31370  elpjrn  31443  ofrn2  31865  off2  31866  ofresid  31867  xppreima2  31876  ofpreima2  31891  suppovss  31906  resf1o  31955  swrdrn3  32119  pwrssmgc  32170  mgcf1o  32173  gsumhashmul  32208  gsumle  32242  symgcom2  32245  pmtrcnel  32250  pmtrcnel2  32251  pmtrcnelor  32252  cycpmfvlem  32271  cycpmfv3  32274  cycpmcl  32275  cycpmco2rn  32284  cycpmco2  32292  cycpm3cl2  32295  cyc3co2  32299  cyc3evpm  32309  islinds5  32480  ellspds  32481  ghmquskerlem1  32528  ghmquskerco  32529  ghmquskerlem3  32531  ghmqusker  32532  rhmpreimaidl  32537  elrspunidl  32546  elrspunsn  32547  rhmimaidl  32550  rhmpreimaprmidl  32570  evls1fn  32640  evls1fpws  32646  ressply1evl  32647  ply1degltel  32666  ply1degltlss  32667  ply1gsumz  32669  ig1pmindeg  32671  ply1degltdimlem  32707  ply1degltdim  32708  dimkerim  32712  fedgmullem2  32715  fedgmul  32716  irngss  32751  irngnzply1  32755  irngnminplynz  32771  cmpcref  32830  rhmpreimacnlem  32864  fsumcvg4  32930  pl1cn  32935  qqhval2lem  32961  prodindf  33021  indpreima  33023  esumcvg  33084  ofcf  33101  ofcof  33105  measfn  33202  meascnbl  33217  sibfof  33339  sitgaddlemb  33347  subiwrdlen  33385  rrvfn  33444  plymul02  33557  signsplypnf  33561  signsply0  33562  reprsuc  33627  reprdifc  33639  breprexplema  33642  circlemethhgt  33655  hgt750lemb  33668  f1resrcmplf1dlem  34089  pthhashvtx  34118  cvmopnlem  34269  cvmliftmolem1  34272  cvmliftlem10  34285  cvmlift2lem9a  34294  cvmlift2lem6  34299  cvmlift2lem12  34305  cvmliftphtlem  34308  cvmlift3lem9  34318  mrsubrn  34504  elmrsubrn  34511  elmsubrn  34519  msubrn  34520  mclsind  34561  mclsppslem  34574  mclspps  34575  iprodefisumlem  34710  gg-dvmulbr  35175  matunitlindflem1  36484  poimirlem1  36489  poimirlem2  36490  poimirlem3  36491  poimirlem16  36504  poimirlem17  36505  poimirlem19  36507  poimirlem20  36508  poimirlem22  36510  poimirlem23  36511  poimirlem29  36517  poimirlem30  36518  poimirlem31  36519  poimir  36521  mblfinlem2  36526  itg2addnclem3  36541  itg2addnc  36542  itg2gt0cn  36543  ftc1cnnc  36560  ftc1anclem5  36565  ftc1anclem7  36567  ftc1anc  36569  sdclem2  36610  istotbnd3  36639  sstotbnd2  36642  isbnd3  36652  heibor1lem  36677  rrnmet  36697  grpokerinj  36761  isdrngo2  36826  lfl1  37940  lfladdcl  37941  lflvscl  37947  lkr0f  37964  lkrsc  37967  eqlkr2  37970  eqlkr3  37971  ldualvaddval  38001  ldualvsval  38008  tendoeq1  39635  sticksstones1  40962  sticksstones2  40963  sticksstones3  40964  sticksstones12a  40973  sticksstones12  40974  metakunt19  41003  metakunt25  41009  metakunt33  41017  frlmvscadiccat  41080  frlmsnic  41110  pwsgprod  41114  mplmapghm  41128  evlsvvval  41135  evlsaddval  41140  evlsmulval  41141  evladdval  41147  evlmulval  41148  selvvvval  41157  evlselvlem  41158  evlselv  41159  fsuppssind  41165  mhphf  41169  ismrcd1  41436  ismrcd2  41437  istopclsd  41438  isnacs3  41448  mzpaddmpt  41479  mzpmulmpt  41480  mzpsubst  41486  mzpcong  41711  fnwe2lem2  41793  islmodfg  41811  kercvrlsm  41825  dgrsub2  41877  mpaaeu  41892  rngunsnply  41915  idomrootle  41937  hausgraph  41954  ofoafg  42104  ofoafo  42106  ofoaid1  42108  ofoaid2  42109  naddcnff  42112  naddcnffn  42113  naddcnffo  42114  naddcnfcom  42116  naddcnfid1  42117  naddcnfass  42119  fsovf1od  42767  brcoffn  42781  clsneiel1  42859  wfximgfd  42915  extoimad  42916  mnringmulrcld  42987  mnurndlem1  43040  caofcan  43082  ofmul12  43084  ofdivrec  43085  ofdivcan4  43086  ofdivdiv2  43087  dvconstbi  43093  binomcxplemnotnn0  43115  refsum2cnlem1  43721  ssmapsn  43915  preimaiocmnf  44274  fsumsupp0  44294  fsumsermpt  44295  climinf  44322  climinf2lem  44422  limsupmnflem  44436  limsupvaluz2  44454  supcnvlimsup  44456  limsupgtlem  44493  liminfvalxr  44499  liminflelimsupuz  44501  xlimconst2  44551  climxlim2  44562  icccncfext  44603  dvnprodlem1  44662  volicoff  44711  voliooicof  44712  fourierdlem25  44848  etransclem2  44952  etransclem35  44985  fge0iccico  45086  sge0tsms  45096  sge0sup  45107  sge0resrn  45120  sge0le  45123  sge0fodjrnlem  45132  sge0isum  45143  sge0seq  45162  nnfoctbdjlem  45171  meadjiunlem  45181  omeiunle  45233  hoicvr  45264  ovolval4lem1  45365  ovolval5lem3  45370  ovnovollem1  45372  ovnovollem2  45373  iinhoiicclem  45389  iunhoiioolem  45391  preimaicomnf  45427  smfresal  45504  smfsuplem1  45527  smflimsuplem2  45537  fcoreslem3  45775  fcoreslem4  45776  fcores  45777  mgmhmf1o  46557  resmgmhm2b  46570  mgmhmima  46572  mgmhmeql  46573  prdsmulrngcl  46676  prdsrngd  46677  rnghmf1o  46701  rhmimasubrnglem  46744  ackvalsucsucval  47374  amgmwlem  47849