Theorem ffnd 6708

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

This proof depends on syntax axioms:   → wi 4   Fn wfn 6532  ⟶wf 6533

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 6541

This theorem is used by:  fnconstg  6768  f1fn  6777  fofn  6796  f1ofn  6823  feqmptd  6951  fssrescdmd  7125  fprb  7197  f1resrcmplf1dlem  7276  cocan1  7297  oprres  7586  off  7709  coof  7715  ofco  7716  caofref  7722  caofid0l  7724  caofid0r  7725  caofid1  7726  caofid2  7727  caofrss  7730  caoftrn  7732  fo2ndf  8130  fnwelem  8141  fnse  8143  suppsnop  8188  suppss  8204  suppssr  8205  suppssrg  8206  suppssof1  8209  suppofssd  8213  suppofss1d  8214  suppofss2d  8215  suppcoss  8217  smocdmdom  8369  elmapfn  8880  ralxpmap  8917  omxpenlem  9090  mapen  9153  f1finf1o  9257  unirnffid  9329  fdmfifsupp  9360  mapfien  9393  intrnfi  9401  marypha2  9424  ordtypelem7  9511  wemapsolem  9537  wemapso  9538  wemapso2lem  9539  unxpwdom2  9575  ixpiunwdom  9577  cantnfle  9665  cantnfp1lem2  9673  cantnfp1lem3  9674  cantnfp1  9675  oemapvali  9678  cantnflem1a  9679  cantnflem1c  9681  cantnflem3  9685  cantnf  9687  cnfcomlem  9693  cnfcom3  9698  updjudhcoinlf  10006  updjudhcoinrg  10007  fseqenlem1  10096  numacn  10121  infpwfien  10134  isf32lem2  10425  isf34lem7  10450  isf34lem6  10451  unirnfdomd  10645  ofsubeq0  12310  ofnegsub  12311  ofsubge0  12312  seqf1olem2  14178  resunimafz0  14583  wrdfn  14666  swrdvalfn  14793  swrdrn3  14795  pfxfn  14824  pfxid  14827  cats1un  14863  cshwfn  14945  ccatco  14979  limsupgle  15637  o1of2  15773  o1rlimmul  15779  isercolllem2  15826  isercoll  15828  isercoll2  15829  climsup  15830  fsumss  15884  ruclem11  16401  vdwlem2  17153  vdwlem6  17157  vdwlem9  17160  vdwlem12  17163  0ram  17191  ramub1lem1  17197  pwsle  17657  pwsleval  17658  pwsvscaval  17660  mrcuni  17788  mrcun  17789  invf1o  17937  funcres2c  18071  setcmon  18255  setcepi  18256  uncfcurf  18406  yoniso  18452  isacs4lem  18711  acsmapd  18721  chnso  18791  mgmn0plusgplusf  18821  gsumval2  18868  mgmhmf1o  18882  resmgmhm2b  18895  mgmhmima  18897  mgmhmeql  18898  prdsplusgsgrpcl  18914  prdssgrpd  18915  prdsplusgcl  18955  prdsidlem  18956  prdsmndd  18957  mhmf1o  18984  resmhm2b  19011  mhmimalem  19013  mhmima  19014  mhmeql  19015  prdspjmhm  19018  pwsco1mhm  19021  pwsco2mhm  19022  gsumwmhm  19034  frmdss2  19052  grpinvf1o  19212  prdsinvlem  19252  cycsubgcl  19414  ghmrn  19436  ghmpreima  19445  ghmeql  19446  ghmnsgima  19447  ghmnsgpreima  19448  ghmeqker  19450  ghmf1o  19455  ghmqusnsglem1  19487  ghmqusnsg  19489  ghmquskerlem1  19490  ghmquskerco  19491  ghmquskerlem3  19493  ghmqusker  19494  gass  19508  cntzmhm  19548  symgextres  19632  gsmsymgrfixlem1  19634  fvcosymgeq  19636  f1omvdconj  19653  pmtrfinv  19668  symgtrinv  19679  pmtr3ncomlem1  19680  sygbasnfpfi  19719  efginvrel2  19934  efgredleme  19950  ghmplusg  20053  prdscmnd  20068  gsumval3a  20110  gsumval3eu  20111  gsumzaddlem  20128  gsumzsplit  20134  gsumpt  20169  prdsgsum  20188  dprdfcntz  20224  dprdfadd  20229  dprdfeq0  20231  dprdf11  20232  dprdlub  20235  dprdspan  20236  dprd2dlem1  20250  dmdprdpr  20258  dprdpr  20259  dpjlem  20260  ablfac1eu  20282  gsumle  20352  prdsmulrngcl  20390  prdsrngd  20391  prdsringd  20543  prdscrngd  20544  prds1  20545  pwspjmhmmgpd  20550  pwsgprod  20552  rnghmf1o  20675  rhmf1o  20720  rhmimasubrnglem  20810  rnrhmsubrg  20850  rrgsupp  20946  imadrhmcl  21047  isabvd  21062  lmodfopnelem1  21166  lcomfsupp  21170  prdsvscacl  21236  prdslmodd  21237  lmhmco  21311  lmhmplusg  21312  lmhmvsca  21313  lmhmf1o  21314  lmhmeql  21323  lspextmo  21324  rhmpreimaidl  21564  rhmpreimaprmidl  21628  pjfo  22014  dsmmbas2  22036  dsmm0cl  22039  dsmmacl  22040  dsmmsubg  22042  dsmmlss  22043  frlmvplusgvalc  22066  frlmvscaval  22067  frlmplusgvalb  22068  frlmvscavalb  22069  frlmsslss2  22074  frlmphllem  22079  frlmphl  22080  frlmssuvc2  22094  frlmsslsp  22095  frlmup1  22097  frlmup2  22098  frlmup3  22099  frlmup4  22100  islindf4  22137  psrbagfsupp  22220  psrbaglesupp  22223  psrbaglecl  22224  psrbagaddcl  22225  psrbagcon  22226  psrbaglefi  22227  psrbagleadd1  22229  psrbagconf1o  22230  gsumbagdiaglem  22232  psrass1lem  22234  psrvscaval  22251  psrlidm  22262  psrridm  22263  psrass1  22264  psrdi  22265  psrdir  22266  psrascl  22279  mvrf2  22293  mplsubglem  22299  mplvscaval  22316  subrgmvrf  22336  mplbas2  22344  mplind  22372  psrbagev1  22379  psrbagev2  22380  evlslem3  22382  evlslem1  22384  evlsvvval  22395  evlsvar  22397  evladdval  22405  evlmulval  22406  mpfind  22417  mplmapghm  22424  evlsaddval  22431  evlsmulval  22432  selvvvval  22444  ismhp3  22456  mhpmulcl  22463  psdmplcl  22476  psdadd  22477  psdvsca  22478  psdmul  22480  psdmvr  22483  psrplusgpropd  22546  coe1add  22576  coe1addfv  22577  evl1addd  22652  evl1subd  22653  evl1muld  22654  pf1mpf  22663  pf1ind  22666  evls1fpws  22680  ressply1evl  22681  rhmply1vsca  22696  mamudir  22712  mamulid  22749  mamurid  22750  mdetrlin  22910  mdetrsca  22911  mdetralt  22916  mdetunilem7  22926  mdetunilem9  22928  madurid  22952  matunitlindflem1  22987  cnrest2  23597  lmss  23609  lmcnp  23615  cnt0  23657  cnt1  23661  cnhaus  23665  rncmp  23707  conncn  23737  2ndcomap  23770  1stccnp  23774  comppfsc  23844  1stckgenlem  23865  ptbasfi  23893  ptopn  23895  ptclsg  23927  ptcnp  23934  upxp  23935  txtube  23952  txcmplem1  23953  hauseqlcld  23958  xkohaus  23965  xkoptsub  23966  cnmpt11  23975  cnmpt21  23983  cnmpt22f  23987  cnmptcom  23990  qtopss  24027  qtopeu  24028  qtopomap  24030  qtopcmap  24031  kqffn  24037  hmeof1o2  24075  xkocnv  24126  rnelfm  24265  ptcmplem1  24364  cnextfres1  24380  ghmcnp  24427  tgphaus  24429  prdstmdd  24436  prdstgpd  24437  fmucnd  24603  psmetxrge0  24625  isxmet2d  24639  prdsmet  24682  blelrnps  24728  blelrn  24729  xmetresbl  24749  comet  24825  stdbdxmet  24827  met2ndci  24834  prdsxmslem2  24841  isngp3  24910  nmotri  25051  metdsre  25166  bndth  25272  evth  25273  fmcfil  25586  bcthlem4  25641  rrxcph  25706  rrxds  25707  rrxmet  25722  evthicc2  25774  ovolfsf  25785  ovolmge0  25791  ovollb2lem  25802  ovolunlem1a  25810  ovoliunlem1  25816  ovoliun  25819  ovoliun2  25820  ovolscalem1  25827  ovolicc1  25830  ovolicc2lem4  25834  ovolicc2  25836  voliunlem1  25864  voliunlem3  25866  volsup  25870  ioombl1lem2  25873  ioombl1lem4  25875  uniiccdif  25892  uniioombllem2  25897  uniioombllem3  25899  uniioombllem6  25902  volsup2  25919  vitalilem4  25925  mbfeqalem1  25955  mbfmulc2lem  25961  mbfmax  25963  mbfaddlem  25974  mbfadd  25975  mbfsub  25976  mbfsup  25978  mbfinf  25979  itg1ge0  26000  itg1addlem1  26006  i1faddlem  26007  i1fmullem  26008  i1fadd  26009  i1fmul  26010  itg1addlem4  26013  i1fmulclem  26016  i1fmulc  26017  itg1mulc  26018  i1fres  26019  itg10a  26024  itg1ge0a  26025  itg1lea  26026  mbfi1fseqlem3  26031  mbfi1fseqlem4  26032  mbfi1flimlem  26036  mbfmullem2  26038  mbfmul  26040  itg20  26051  itg2lea  26058  itg2splitlem  26062  itg2split  26063  itg2monolem1  26064  itg2monolem2  26065  itg2monolem3  26066  itg2mono  26067  itg2i1fseqle  26068  itg2i1fseq  26069  itg2addlem  26072  itg2gt0  26074  itg2cnlem1  26075  itg2cnlem2  26076  itg2cn  26077  itgitg1  26122  bddmulibl  26152  bddibl  26153  dvidlem  26228  dvaddbr  26251  dvmulbr  26252  dvaddf  26255  dvcmulf  26258  dvrec  26268  dvcnvlem  26289  rolle  26303  dveq0  26313  dv11cn  26314  dvivthlem2  26322  dvivth  26323  dvne0  26324  lhop1lem  26326  lhop1  26327  lhop2  26328  lhop  26329  ftc1cn  26356  tdeglem1  26369  tdeglem3  26370  tdeglem4  26371  mdegleb  26375  mdegldg  26377  mdegaddle  26385  ply1remlem  26476  ply1rem  26477  fta1glem1  26479  fta1glem2  26480  fta1blem  26482  idomrootle  26484  plyeq0lem  26522  plyeq0  26523  plyaddlem1  26525  coeeulem  26536  coeaddlem  26561  coemulc  26567  dgradd2  26580  dgrcolem2  26586  ofmulrt  26593  plymul02  26594  plyrem  26619  rnplynfin  26623  plyconz  26624  vieta1lem1  26626  vieta1  26628  plyexmo  26629  elqaalem3  26637  aannenlem1  26648  aalioulem2  26653  ulmuni  26712  ulmdvlem1  26720  ulmdv  26723  mbfulm  26726  iblulm  26727  itgulm  26728  rlimcnp2  27287  jensen  27309  amgm  27311  basellem3  27403  basellem7  27407  basellem9  27409  dchrelbas2  27557  dchrmulcl  27569  dchrfi  27575  dchreq  27578  dchrresb  27579  dchrinv  27581  dchr1re  27583  sumdchr2  27590  dchr2sum  27593  lgsqrlem2  27667  lgsqrlem3  27668  rpvmasum2  27832  dchrisum0re  27833  mirf1o  29134  lmif1o  29293  elcgrabasi  29368  eqeefv  29474  axlowdimlem14  29526  vtxdgfisf  30050  pthhashvtx  30308  2pthon3v  30525  nvinvfval  31235  sspg  31323  ssps  31325  sspmlem  31327  sspn  31331  lnon0  31393  ubthlem1  31465  pjfn  32304  kbpj  32551  kbass2  32712  elpjrn  32785  ofrn2  33227  off2  33228  ofresid  33229  xppreima2  33238  ofpreima2  33253  suppovss  33267  resf1o  33315  prodindf  33422  indpreima  33425  pwrssmgc  33554  mgcf1o  33557  gsumfs2d  33615  gsumhashmul  33621  symgcom2  33638  pmtrcnel  33643  pmtrcnel2  33644  pmtrcnelor  33645  cycpmfvlem  33666  cycpmfv3  33669  cycpmcl  33670  cycpmco2rn  33679  cycpmco2  33687  cycpm3cl2  33690  cyc3co2  33694  cyc3evpm  33704  elrgspnlem1  33796  elrgspnlem2  33797  elrgspnlem4  33799  elrgspnsubrunlem1  33801  elrgspnsubrunlem2  33802  gsumind  33899  islinds5  33916  ellspds  33917  elrspunidl  33971  elrspunsn  33972  rhmimaidl  33975  rprmdvdsprod  34059  1arithidomlem2  34061  evls1fn  34085  ply1dg1rt  34105  ply1mulrtss  34107  ply1degltel  34119  ply1degleel  34120  ply1degltlss  34121  ply1gsumz  34124  ig1pmindeg  34127  r1pquslmic  34135  0mplrim  34139  mplasclco  34141  selvply1rhmlema  34143  selvply1rhmlemb  34144  selvply1rhmlem1  34145  selvply1rhmlem4  34148  selvply1rhm0  34151  extvfvcl  34161  mplmulmvr  34164  evlextv  34167  mplvrpmmhm  34171  mplvrpmrhm  34172  psrmonprod  34177  esplyfval0  34189  esplyfval2  34190  esplyfv1  34194  esplyfv  34195  esplyfval3  34197  esplyfvaln  34199  esplyind  34200  vieta  34205  exsslsb  34222  ply1degltdimlem  34247  ply1degltdim  34248  dimkerim  34252  fedgmullem2  34255  fedgmul  34256  lvecendof1f1o  34258  fldextrspunlsplem  34298  fldextrspunlsp  34299  irngss  34312  irngnzply1  34316  extdgfialglem2  34318  irngnminplynz  34337  2sqr3minply  34405  cos9thpiminply  34413  cmpcref  34475  rhmpreimacnlem  34509  fsumcvg4  34575  pl1cn  34580  qqhval2lem  34606  esumcvg  34711  ofcf  34728  ofcof  34732  measfn  34830  meascnbl  34845  sibfof  34965  sitgaddlemb  34973  subiwrdlen  35011  rrvfn  35070  signsplypnf  35172  signsply0  35173  reprsuc  35237  reprdifc  35249  breprexplema  35252  circlemethhgt  35265  hgt750lemb  35278  cvmopnlem  36022  cvmliftmolem1  36025  cvmliftlem10  36038  cvmlift2lem9a  36047  cvmlift2lem6  36052  cvmlift2lem12  36058  cvmliftphtlem  36061  cvmlift3lem9  36071  mrsubrn  36257  elmrsubrn  36264  elmsubrn  36272  msubrn  36273  mclsind  36314  mclsppslem  36327  mclspps  36328  iprodefisumlem  36484  weiunfrlem  37232  mh-inf3f1  37309  poimirlem1  38519  poimirlem2  38520  poimirlem3  38521  poimirlem16  38534  poimirlem17  38535  poimirlem19  38537  poimirlem20  38538  poimirlem22  38540  poimirlem23  38541  poimirlem29  38547  poimirlem30  38548  poimirlem31  38549  poimir  38551  mblfinlem2  38556  itg2addnclem3  38571  itg2addnc  38572  itg2gt0cn  38573  ftc1cnnc  38590  ftc1anclem5  38595  ftc1anclem7  38597  ftc1anc  38599  sdclem2  38656  istotbnd3  38685  sstotbnd2  38688  isbnd3  38698  heibor1lem  38723  rrnmet  38743  grpokerinj  38807  isdrngo2  38872  lfl1  40107  lfladdcl  40108  lflvscl  40114  lkr0f  40131  lkrsc  40134  eqlkr2  40137  eqlkr3  40138  ldualvaddval  40168  ldualvsval  40175  tendoeq1  41801  zndvdchrrhm  43003  hashscontpow  43152  aks6d1c3  43153  aks6d1c2lem4  43157  aks6d1c2  43160  sticksstones1  43176  sticksstones2  43177  sticksstones3  43178  sticksstones12a  43187  sticksstones12  43188  aks6d1c6lem2  43201  aks6d1c6lem3  43202  aks6d1c6isolem1  43204  aks6d1c6isolem3  43206  aks6d1c6lem5  43207  aks6d1c7lem1  43210  unitscyglem1  43225  dvun  43390  frlmbasfn  43545  frlmvscadiccat  43553  fiabv  43580  frlmsnic  43584  evlselvlem  43596  evlselv  43597  fsuppssind  43601  mhphf  43605  ismrcd1  43688  ismrcd2  43689  istopclsd  43690  isnacs3  43700  mzpaddmpt  43731  mzpmulmpt  43732  mzpsubst  43738  mzpcong  43958  fnwe2lem2  44037  islmodfg  44055  kercvrlsm  44069  dgrsub2  44121  mpaaeu  44136  rngunsnply  44155  hausgraph  44191  ofoafg  44340  ofoafo  44342  ofoaid1  44344  ofoaid2  44345  naddcnff  44348  naddcnffn  44349  naddcnffo  44350  naddcnfcom  44352  naddcnfid1  44353  naddcnfass  44355  fsovf1od  45001  brcoffn  45015  clsneiel1  45093  wfximgfd  45148  extoimad  45149  mnringmulrcld  45211  mnurndlem1  45250  caofcan  45292  ofmul12  45294  ofdivrec  45295  ofdivcan4  45296  ofdivdiv2  45297  dvconstbi  45303  binomcxplemnotnn0  45325  relpmin  45920  refsum2cnlem1  46023  ssmapsn  46198  preimaiocmnf  46541  fsumsupp0  46559  fsumsermpt  46560  climinf  46587  climinf2lem  46685  limsupmnflem  46699  limsupvaluz2  46717  supcnvlimsup  46719  limsupgtlem  46756  liminfvalxr  46762  liminflelimsupuz  46764  xlimconst2  46814  climxlim2  46825  icccncfext  46866  dvnprodlem1  46925  volicoff  46974  voliooicof  46975  fourierdlem25  47111  fourierdlem48  47133  fourierdlem49  47134  etransclem2  47215  etransclem35  47248  fge0iccico  47349  sge0tsms  47359  sge0sup  47370  sge0resrn  47383  sge0le  47386  sge0fodjrnlem  47395  sge0isum  47406  sge0seq  47425  nnfoctbdjlem  47434  meadjiunlem  47444  omeiunle  47496  hoicvr  47527  ovolval4lem1  47628  ovolval5lem3  47633  ovnovollem1  47635  ovnovollem2  47636  iinhoiicclem  47652  iunhoiioolem  47654  preimaicomnf  47690  smfresal  47767  smfsuplem1  47790  smflimsuplem2  47800  tmachlem-franscan  47928  fcoreslem3  48104  fcoreslem4  48105  fcores  48106  isubgredg  48933  upgrimpths  48976  ackvalsucsucval  49769  funchomf  50174  imasubc  50228  imassc  50230  imaid  50231  prcofdiag1  50470  prcofdiag  50471  oppfdiag1  50491  oppfdiag  50493  crossp3d  50936  veroquadmodzerod  50953  amgmwlem  50956