Theorem ffnd 6703

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

This proof depends on syntax axioms:   → wi 4   Fn wfn 6528  ⟶wf 6529

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 6537

This theorem is used by:  fnconstg  6763  f1fn  6772  fofn  6791  f1ofn  6818  feqmptd  6946  fssrescdmd  7120  fprb  7192  f1resrcmplf1dlem  7271  cocan1  7292  oprres  7581  off  7696  coof  7702  ofco  7703  caofref  7709  caofid0l  7711  caofid0r  7712  caofid1  7713  caofid2  7714  caofrss  7717  caoftrn  7719  fo2ndf  8118  fnwelem  8129  fnse  8131  suppsnop  8176  suppss  8192  suppssr  8193  suppssrg  8194  suppssof1  8197  suppofssd  8201  suppofss1d  8202  suppofss2d  8203  suppcoss  8205  smocdmdom  8357  elmapfn  8866  ralxpmap  8903  omxpenlem  9076  mapen  9139  f1finf1o  9243  unirnffid  9314  fdmfifsupp  9345  mapfien  9378  intrnfi  9386  marypha2  9409  ordtypelem7  9496  wemapsolem  9522  wemapso  9523  wemapso2lem  9524  unxpwdom2  9560  ixpiunwdom  9562  cantnfle  9650  cantnfp1lem2  9658  cantnfp1lem3  9659  cantnfp1  9660  oemapvali  9663  cantnflem1a  9664  cantnflem1c  9666  cantnflem3  9670  cantnf  9672  cnfcomlem  9678  cnfcom3  9683  updjudhcoinlf  9937  updjudhcoinrg  9938  fseqenlem1  10027  numacn  10052  infpwfien  10065  isf32lem2  10356  isf34lem7  10381  isf34lem6  10382  unirnfdomd  10576  ofsubeq0  12239  ofnegsub  12240  ofsubge0  12241  seqf1olem2  14106  resunimafz0  14510  wrdfn  14593  swrdvalfn  14720  swrdrn3  14722  pfxfn  14751  pfxid  14754  cats1un  14790  cshwfn  14872  ccatco  14906  limsupgle  15564  o1of2  15700  o1rlimmul  15706  isercolllem2  15753  isercoll  15755  isercoll2  15756  climsup  15757  fsumss  15811  ruclem11  16328  vdwlem2  17074  vdwlem6  17078  vdwlem9  17081  vdwlem12  17084  0ram  17112  ramub1lem1  17118  pwsle  17578  pwsleval  17579  pwsvscaval  17581  mrcuni  17709  mrcun  17710  invf1o  17858  funcres2c  17992  setcmon  18176  setcepi  18177  uncfcurf  18327  yoniso  18373  isacs4lem  18632  acsmapd  18642  chnso  18712  mgmn0plusgplusf  18742  gsumval2  18788  mgmhmf1o  18802  resmgmhm2b  18815  mgmhmima  18817  mgmhmeql  18818  prdsplusgsgrpcl  18834  prdssgrpd  18835  prdsplusgcl  18875  prdsidlem  18876  prdsmndd  18877  mhmf1o  18904  resmhm2b  18931  mhmimalem  18933  mhmima  18934  mhmeql  18935  prdspjmhm  18938  pwsco1mhm  18941  pwsco2mhm  18942  gsumwmhm  18954  frmdss2  18972  grpinvf1o  19132  prdsinvlem  19172  cycsubgcl  19334  ghmrn  19356  ghmpreima  19365  ghmeql  19366  ghmnsgima  19367  ghmnsgpreima  19368  ghmeqker  19370  ghmf1o  19375  ghmqusnsglem1  19407  ghmqusnsg  19409  ghmquskerlem1  19410  ghmquskerco  19411  ghmquskerlem3  19413  ghmqusker  19414  gass  19428  cntzmhm  19468  symgextres  19552  gsmsymgrfixlem1  19554  fvcosymgeq  19556  f1omvdconj  19573  pmtrfinv  19588  symgtrinv  19599  pmtr3ncomlem1  19600  sygbasnfpfi  19639  efginvrel2  19854  efgredleme  19870  ghmplusg  19973  prdscmnd  19988  gsumval3a  20030  gsumval3eu  20031  gsumzaddlem  20048  gsumzsplit  20054  gsumpt  20089  prdsgsum  20108  dprdfcntz  20144  dprdfadd  20149  dprdfeq0  20151  dprdf11  20152  dprdlub  20155  dprdspan  20156  dprd2dlem1  20170  dmdprdpr  20178  dprdpr  20179  dpjlem  20180  ablfac1eu  20202  gsumle  20272  prdsmulrngcl  20310  prdsrngd  20311  prdsringd  20461  prdscrngd  20462  prds1  20463  pwspjmhmmgpd  20468  pwsgprod  20470  rnghmf1o  20593  rhmf1o  20638  rhmimasubrnglem  20727  rnrhmsubrg  20767  rrgsupp  20863  imadrhmcl  20963  isabvd  20978  lmodfopnelem1  21082  lcomfsupp  21086  prdsvscacl  21152  prdslmodd  21153  lmhmco  21227  lmhmplusg  21228  lmhmvsca  21229  lmhmf1o  21230  lmhmeql  21239  lspextmo  21240  rhmpreimaidl  21479  rhmpreimaprmidl  21542  pjfo  21928  dsmmbas2  21950  dsmm0cl  21953  dsmmacl  21954  dsmmsubg  21956  dsmmlss  21957  frlmvplusgvalc  21980  frlmvscaval  21981  frlmplusgvalb  21982  frlmvscavalb  21983  frlmsslss2  21988  frlmphllem  21993  frlmphl  21994  frlmssuvc2  22008  frlmsslsp  22009  frlmup1  22011  frlmup2  22012  frlmup3  22013  frlmup4  22014  islindf4  22051  psrbagfsupp  22134  psrbaglesupp  22137  psrbaglecl  22138  psrbagaddcl  22139  psrbagcon  22140  psrbaglefi  22141  psrbagleadd1  22143  psrbagconf1o  22144  gsumbagdiaglem  22146  psrass1lem  22148  psrvscaval  22165  psrlidm  22176  psrridm  22177  psrass1  22178  psrdi  22179  psrdir  22180  psrascl  22193  mvrf2  22207  mplsubglem  22213  mplvscaval  22230  subrgmvrf  22250  mplbas2  22258  mplind  22286  psrbagev1  22293  psrbagev2  22294  evlslem3  22296  evlslem1  22298  evlsvvval  22309  evlsvar  22311  evladdval  22319  evlmulval  22320  mpfind  22331  mplmapghm  22338  evlsaddval  22345  evlsmulval  22346  selvvvval  22358  ismhp3  22370  mhpmulcl  22377  psdmplcl  22390  psdadd  22391  psdvsca  22392  psdmul  22394  psdmvr  22397  psrplusgpropd  22460  coe1add  22490  coe1addfv  22491  evl1addd  22566  evl1subd  22567  evl1muld  22568  pf1mpf  22577  pf1ind  22580  evls1fpws  22594  ressply1evl  22595  rhmply1vsca  22610  mamudir  22626  mamulid  22663  mamurid  22664  mdetrlin  22824  mdetrsca  22825  mdetralt  22830  mdetunilem7  22840  mdetunilem9  22842  madurid  22866  matunitlindflem1  22901  cnrest2  23511  lmss  23523  lmcnp  23529  cnt0  23571  cnt1  23575  cnhaus  23579  rncmp  23621  conncn  23651  2ndcomap  23684  1stccnp  23688  comppfsc  23758  1stckgenlem  23779  ptbasfi  23807  ptopn  23809  ptclsg  23841  ptcnp  23848  upxp  23849  txtube  23866  txcmplem1  23867  hauseqlcld  23872  xkohaus  23879  xkoptsub  23880  cnmpt11  23889  cnmpt21  23897  cnmpt22f  23901  cnmptcom  23904  qtopss  23941  qtopeu  23942  qtopomap  23944  qtopcmap  23945  kqffn  23951  hmeof1o2  23989  xkocnv  24040  rnelfm  24179  ptcmplem1  24278  cnextfres1  24294  ghmcnp  24341  tgphaus  24343  prdstmdd  24350  prdstgpd  24351  fmucnd  24517  psmetxrge0  24539  isxmet2d  24553  prdsmet  24596  blelrnps  24642  blelrn  24643  xmetresbl  24663  comet  24739  stdbdxmet  24741  met2ndci  24748  prdsxmslem2  24755  isngp3  24824  nmotri  24965  metdsre  25080  bndth  25186  evth  25187  fmcfil  25500  bcthlem4  25555  rrxcph  25620  rrxds  25621  rrxmet  25636  evthicc2  25688  ovolfsf  25699  ovolmge0  25705  ovollb2lem  25716  ovolunlem1a  25724  ovoliunlem1  25730  ovoliun  25733  ovoliun2  25734  ovolscalem1  25741  ovolicc1  25744  ovolicc2lem4  25748  ovolicc2  25750  voliunlem1  25778  voliunlem3  25780  volsup  25784  ioombl1lem2  25787  ioombl1lem4  25789  uniiccdif  25806  uniioombllem2  25811  uniioombllem3  25813  uniioombllem6  25816  volsup2  25833  vitalilem4  25839  mbfeqalem1  25869  mbfmulc2lem  25875  mbfmax  25877  mbfaddlem  25888  mbfadd  25889  mbfsub  25890  mbfsup  25892  mbfinf  25893  itg1ge0  25914  itg1addlem1  25920  i1faddlem  25921  i1fmullem  25922  i1fadd  25923  i1fmul  25924  itg1addlem4  25927  i1fmulclem  25930  i1fmulc  25931  itg1mulc  25932  i1fres  25933  itg10a  25938  itg1ge0a  25939  itg1lea  25940  mbfi1fseqlem3  25945  mbfi1fseqlem4  25946  mbfi1flimlem  25950  mbfmullem2  25952  mbfmul  25954  itg20  25965  itg2lea  25972  itg2splitlem  25976  itg2split  25977  itg2monolem1  25978  itg2monolem2  25979  itg2monolem3  25980  itg2mono  25981  itg2i1fseqle  25982  itg2i1fseq  25983  itg2addlem  25986  itg2gt0  25988  itg2cnlem1  25989  itg2cnlem2  25990  itg2cn  25991  itgitg1  26036  bddmulibl  26066  bddibl  26067  dvidlem  26142  dvaddbr  26165  dvmulbr  26166  dvaddf  26169  dvcmulf  26172  dvrec  26182  dvcnvlem  26203  rolle  26217  dveq0  26227  dv11cn  26228  dvivthlem2  26236  dvivth  26237  dvne0  26238  lhop1lem  26240  lhop1  26241  lhop2  26242  lhop  26243  ftc1cn  26270  tdeglem1  26283  tdeglem3  26284  tdeglem4  26285  mdegleb  26289  mdegldg  26291  mdegaddle  26299  ply1remlem  26390  ply1rem  26391  fta1glem1  26393  fta1glem2  26394  fta1blem  26396  idomrootle  26398  plyeq0lem  26436  plyeq0  26437  plyaddlem1  26439  coeeulem  26450  coeaddlem  26475  coemulc  26481  dgradd2  26494  dgrcolem2  26500  ofmulrt  26509  plymul02  26510  plyrem  26535  rnplynfin  26539  plyconz  26540  vieta1lem1  26542  vieta1  26544  plyexmo  26545  elqaalem3  26553  aannenlem1  26564  aalioulem2  26569  ulmuni  26628  ulmdvlem1  26636  ulmdv  26639  mbfulm  26642  iblulm  26643  itgulm  26644  rlimcnp2  27203  jensen  27225  amgm  27227  basellem3  27319  basellem7  27323  basellem9  27325  dchrelbas2  27473  dchrmulcl  27485  dchrfi  27491  dchreq  27494  dchrresb  27495  dchrinv  27497  dchr1re  27499  sumdchr2  27506  dchr2sum  27509  lgsqrlem2  27583  lgsqrlem3  27584  rpvmasum2  27748  dchrisum0re  27749  mirf1o  29020  lmif1o  29179  elcgrabasi  29254  eqeefv  29360  axlowdimlem14  29412  vtxdgfisf  29936  pthhashvtx  30194  2pthon3v  30411  nvinvfval  31121  sspg  31209  ssps  31211  sspmlem  31213  sspn  31217  lnon0  31279  ubthlem1  31351  pjfn  32190  kbpj  32437  kbass2  32598  elpjrn  32671  ofrn2  33113  off2  33114  ofresid  33115  xppreima2  33124  ofpreima2  33139  suppovss  33153  resf1o  33201  prodindf  33308  indpreima  33311  pwrssmgc  33440  mgcf1o  33443  gsumfs2d  33501  gsumhashmul  33507  symgcom2  33524  pmtrcnel  33529  pmtrcnel2  33530  pmtrcnelor  33531  cycpmfvlem  33552  cycpmfv3  33555  cycpmcl  33556  cycpmco2rn  33565  cycpmco2  33573  cycpm3cl2  33576  cyc3co2  33580  cyc3evpm  33590  elrgspnlem1  33682  elrgspnlem2  33683  elrgspnlem4  33685  elrgspnsubrunlem1  33687  elrgspnsubrunlem2  33688  gsumind  33785  islinds5  33802  ellspds  33803  elrspunidl  33856  elrspunsn  33857  rhmimaidl  33860  rprmdvdsprod  33944  1arithidomlem2  33946  evls1fn  33970  ply1dg1rt  33990  ply1mulrtss  33992  ply1degltel  34004  ply1degleel  34005  ply1degltlss  34006  ply1gsumz  34009  ig1pmindeg  34012  r1pquslmic  34020  0mplrim  34024  mplasclco  34026  selvply1rhmlema  34028  selvply1rhmlemb  34029  selvply1rhmlem1  34030  selvply1rhmlem4  34033  selvply1rhm0  34036  extvfvcl  34046  mplmulmvr  34049  evlextv  34052  mplvrpmmhm  34056  mplvrpmrhm  34057  psrmonprod  34062  esplyfval0  34074  esplyfval2  34075  esplyfv1  34079  esplyfv  34080  esplyfval3  34082  esplyfvaln  34084  esplyind  34085  vieta  34090  exsslsb  34107  ply1degltdimlem  34132  ply1degltdim  34133  dimkerim  34137  fedgmullem2  34140  fedgmul  34141  lvecendof1f1o  34143  fldextrspunlsplem  34183  fldextrspunlsp  34184  irngss  34197  irngnzply1  34201  extdgfialglem2  34203  irngnminplynz  34222  2sqr3minply  34290  cos9thpiminply  34298  cmpcref  34360  rhmpreimacnlem  34394  fsumcvg4  34460  pl1cn  34465  qqhval2lem  34491  esumcvg  34596  ofcf  34613  ofcof  34617  measfn  34715  meascnbl  34730  sibfof  34851  sitgaddlemb  34859  subiwrdlen  34897  rrvfn  34956  signsplypnf  35058  signsply0  35059  reprsuc  35123  reprdifc  35135  breprexplema  35138  circlemethhgt  35151  hgt750lemb  35164  cvmopnlem  35857  cvmliftmolem1  35860  cvmliftlem10  35873  cvmlift2lem9a  35882  cvmlift2lem6  35887  cvmlift2lem12  35893  cvmliftphtlem  35896  cvmlift3lem9  35906  mrsubrn  36092  elmrsubrn  36099  elmsubrn  36107  msubrn  36108  mclsind  36149  mclsppslem  36162  mclspps  36163  iprodefisumlem  36319  weiunfrlem  37083  mh-inf3f1  37160  poimirlem1  38370  poimirlem2  38371  poimirlem3  38372  poimirlem16  38385  poimirlem17  38386  poimirlem19  38388  poimirlem20  38389  poimirlem22  38391  poimirlem23  38392  poimirlem29  38398  poimirlem30  38399  poimirlem31  38400  poimir  38402  mblfinlem2  38407  itg2addnclem3  38422  itg2addnc  38423  itg2gt0cn  38424  ftc1cnnc  38441  ftc1anclem5  38446  ftc1anclem7  38448  ftc1anc  38450  sdclem2  38492  istotbnd3  38521  sstotbnd2  38524  isbnd3  38534  heibor1lem  38559  rrnmet  38579  grpokerinj  38643  isdrngo2  38708  lfl1  39943  lfladdcl  39944  lflvscl  39950  lkr0f  39967  lkrsc  39970  eqlkr2  39973  eqlkr3  39974  ldualvaddval  40004  ldualvsval  40011  tendoeq1  41637  zndvdchrrhm  42839  hashscontpow  42988  aks6d1c3  42989  aks6d1c2lem4  42993  aks6d1c2  42996  sticksstones1  43012  sticksstones2  43013  sticksstones3  43014  sticksstones12a  43023  sticksstones12  43024  aks6d1c6lem2  43037  aks6d1c6lem3  43038  aks6d1c6isolem1  43040  aks6d1c6isolem3  43042  aks6d1c6lem5  43043  aks6d1c7lem1  43046  unitscyglem1  43061  dvun  43234  frlmvscadiccat  43394  fiabv  43418  frlmsnic  43422  evlselvlem  43434  evlselv  43435  fsuppssind  43439  mhphf  43443  ismrcd1  43543  ismrcd2  43544  istopclsd  43545  isnacs3  43555  mzpaddmpt  43586  mzpmulmpt  43587  mzpsubst  43593  mzpcong  43813  fnwe2lem2  43892  islmodfg  43910  kercvrlsm  43924  dgrsub2  43976  mpaaeu  43991  rngunsnply  44010  hausgraph  44046  ofoafg  44195  ofoafo  44197  ofoaid1  44199  ofoaid2  44200  naddcnff  44203  naddcnffn  44204  naddcnffo  44205  naddcnfcom  44207  naddcnfid1  44208  naddcnfass  44210  fsovf1od  44856  brcoffn  44870  clsneiel1  44948  wfximgfd  45003  extoimad  45004  mnringmulrcld  45066  mnurndlem1  45105  caofcan  45147  ofmul12  45149  ofdivrec  45150  ofdivcan4  45151  ofdivdiv2  45152  dvconstbi  45158  binomcxplemnotnn0  45180  relpmin  45775  refsum2cnlem1  45871  ssmapsn  46046  preimaiocmnf  46390  fsumsupp0  46408  fsumsermpt  46409  climinf  46436  climinf2lem  46534  limsupmnflem  46548  limsupvaluz2  46566  supcnvlimsup  46568  limsupgtlem  46605  liminfvalxr  46611  liminflelimsupuz  46613  xlimconst2  46663  climxlim2  46674  icccncfext  46715  dvnprodlem1  46774  volicoff  46823  voliooicof  46824  fourierdlem25  46960  fourierdlem48  46982  fourierdlem49  46983  etransclem2  47064  etransclem35  47097  fge0iccico  47198  sge0tsms  47208  sge0sup  47219  sge0resrn  47232  sge0le  47235  sge0fodjrnlem  47244  sge0isum  47255  sge0seq  47274  nnfoctbdjlem  47283  meadjiunlem  47293  omeiunle  47345  hoicvr  47376  ovolval4lem1  47477  ovolval5lem3  47482  ovnovollem1  47484  ovnovollem2  47485  iinhoiicclem  47501  iunhoiioolem  47503  preimaicomnf  47539  smfresal  47616  smfsuplem1  47639  smflimsuplem2  47649  tmachlem-franscan  47777  fcoreslem3  47953  fcoreslem4  47954  fcores  47955  isubgredg  48782  upgrimpths  48825  ackvalsucsucval  49618  funchomf  50023  imasubc  50077  imassc  50079  imaid  50080  prcofdiag1  50319  prcofdiag  50320  oppfdiag1  50340  oppfdiag  50342  crossp3d  50800  veroquadmodzerod  50817  amgmwlem  50820