Theorem ffnd 6671

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

Syntax hints:   → wi 4   Fn wfn 6495  ⟶wf 6496

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 6504

This theorem is referenced by:  fnconstg  6730  f1fn  6739  fofn  6756  f1ofn  6783  feqmptd  6910  fssrescdmd  7081  fprb  7150  cocan1  7247  oprres  7536  off  7650  coof  7656  ofco  7657  caofref  7663  caofid0l  7665  caofid0r  7666  caofid1  7667  caofid2  7668  caofrss  7671  caoftrn  7673  fo2ndf  8073  fnwelem  8083  fnse  8085  suppsnop  8130  suppss  8146  suppssr  8147  suppssrg  8148  suppssof1  8151  suppofssd  8155  suppofss1d  8156  suppofss2d  8157  suppcoss  8159  smocdmdom  8310  elmapfn  8814  ralxpmap  8846  omxpenlem  9018  mapen  9081  f1finf1o  9185  unirnffid  9259  fdmfifsupp  9290  mapfien  9323  intrnfi  9331  marypha2  9354  ordtypelem7  9441  wemapsolem  9467  wemapso  9468  wemapso2lem  9469  unxpwdom2  9505  ixpiunwdom  9507  cantnfle  9592  cantnfp1lem2  9600  cantnfp1lem3  9601  cantnfp1  9602  oemapvali  9605  cantnflem1a  9606  cantnflem1c  9608  cantnflem3  9612  cantnf  9614  cnfcomlem  9620  cnfcom3  9625  updjudhcoinlf  9856  updjudhcoinrg  9857  fseqenlem1  9946  numacn  9971  infpwfien  9984  isf32lem2  10276  isf34lem7  10301  isf34lem6  10302  unirnfdomd  10490  ofsubeq0  12154  ofnegsub  12155  ofsubge0  12156  seqf1olem2  13977  resunimafz0  14380  wrdfn  14463  swrdvalfn  14587  pfxfn  14617  pfxid  14620  cats1un  14656  cshwfn  14736  ccatco  14770  limsupgle  15412  o1of2  15548  o1rlimmul  15554  isercolllem2  15601  isercoll  15603  isercoll2  15604  climsup  15605  fsumss  15660  ruclem11  16177  vdwlem2  16922  vdwlem6  16926  vdwlem9  16929  vdwlem12  16932  0ram  16960  ramub1lem1  16966  pwsle  17425  pwsleval  17426  pwsvscaval  17428  mrcuni  17556  mrcun  17557  invf1o  17705  funcres2c  17839  setcmon  18023  setcepi  18024  uncfcurf  18174  yoniso  18220  isacs4lem  18479  acsmapd  18489  chnso  18559  gsumval2  18623  mgmhmf1o  18637  resmgmhm2b  18650  mgmhmima  18652  mgmhmeql  18653  prdsplusgsgrpcl  18669  prdssgrpd  18670  prdsplusgcl  18705  prdsidlem  18706  prdsmndd  18707  mhmf1o  18733  resmhm2b  18759  mhmimalem  18761  mhmima  18762  mhmeql  18763  prdspjmhm  18766  pwsco1mhm  18769  pwsco2mhm  18770  gsumwmhm  18782  frmdss2  18800  grpinvf1o  18951  prdsinvlem  18991  cycsubgcl  19147  ghmrn  19170  ghmpreima  19179  ghmeql  19180  ghmnsgima  19181  ghmnsgpreima  19182  ghmeqker  19184  ghmf1o  19189  ghmqusnsglem1  19221  ghmqusnsg  19223  ghmquskerlem1  19224  ghmquskerco  19225  ghmquskerlem3  19227  ghmqusker  19228  gass  19242  cntzmhm  19282  symgextres  19366  gsmsymgrfixlem1  19368  fvcosymgeq  19370  f1omvdconj  19387  pmtrfinv  19402  symgtrinv  19413  pmtr3ncomlem1  19414  sygbasnfpfi  19453  efginvrel2  19668  efgredleme  19684  ghmplusg  19787  prdscmnd  19802  gsumval3a  19844  gsumval3eu  19845  gsumzaddlem  19862  gsumzsplit  19868  gsumpt  19903  prdsgsum  19922  dprdfcntz  19958  dprdfadd  19963  dprdfeq0  19965  dprdf11  19966  dprdlub  19969  dprdspan  19970  dprd2dlem1  19984  dmdprdpr  19992  dprdpr  19993  dpjlem  19994  ablfac1eu  20016  gsumle  20086  prdsmulrngcl  20122  prdsrngd  20123  prdsringd  20268  prdscrngd  20269  prds1  20270  pwspjmhmmgpd  20275  pwsgprod  20277  rnghmf1o  20400  rhmf1o  20438  rhmimasubrnglem  20510  rnrhmsubrg  20550  rrgsupp  20646  imadrhmcl  20742  isabvd  20757  lmodfopnelem1  20861  lcomfsupp  20865  prdsvscacl  20931  prdslmodd  20932  lmhmco  21007  lmhmplusg  21008  lmhmvsca  21009  lmhmf1o  21010  lmhmeql  21019  lspextmo  21020  rhmpreimaidl  21244  pjfo  21682  dsmmbas2  21704  dsmm0cl  21707  dsmmacl  21708  dsmmsubg  21710  dsmmlss  21711  frlmvplusgvalc  21734  frlmvscaval  21735  frlmplusgvalb  21736  frlmvscavalb  21737  frlmsslss2  21742  frlmphllem  21747  frlmphl  21748  frlmssuvc2  21762  frlmsslsp  21763  frlmup1  21765  frlmup2  21766  frlmup3  21767  frlmup4  21768  islindf4  21805  psrbagfsupp  21887  psrbaglesupp  21890  psrbaglecl  21891  psrbagaddcl  21892  psrbagcon  21893  psrbaglefi  21894  psrbagleadd1  21896  psrbagconf1o  21897  gsumbagdiaglem  21898  psrass1lem  21900  psrvscaval  21918  psrlidm  21929  psrridm  21930  psrass1  21931  psrdi  21932  psrdir  21933  psrascl  21946  mvrf2  21960  mplsubglem  21966  mplvscaval  21983  subrgmvrf  22001  mplbas2  22009  mplind  22037  psrbagev1  22044  psrbagev2  22045  evlslem3  22047  evlslem1  22049  evlsvvval  22060  evlsvar  22062  evladdval  22070  evlmulval  22071  mpfind  22082  ismhp3  22097  mhpmulcl  22104  psdmplcl  22117  psdadd  22118  psdvsca  22119  psdmul  22121  psdmvr  22124  psrplusgpropd  22188  coe1add  22218  coe1addfv  22219  evl1addd  22297  evl1subd  22298  evl1muld  22299  pf1mpf  22308  pf1ind  22311  evls1fpws  22325  ressply1evl  22326  rhmply1vsca  22344  mamudir  22360  mamulid  22397  mamurid  22398  mdetrlin  22558  mdetrsca  22559  mdetralt  22564  mdetunilem7  22574  mdetunilem9  22576  madurid  22600  cnrest2  23242  lmss  23254  lmcnp  23260  cnt0  23302  cnt1  23306  cnhaus  23310  rncmp  23352  conncn  23382  2ndcomap  23414  1stccnp  23418  comppfsc  23488  1stckgenlem  23509  ptbasfi  23537  ptopn  23539  ptclsg  23571  ptcnp  23578  upxp  23579  txtube  23596  txcmplem1  23597  hauseqlcld  23602  xkohaus  23609  xkoptsub  23610  cnmpt11  23619  cnmpt21  23627  cnmpt22f  23631  cnmptcom  23634  qtopss  23671  qtopeu  23672  qtopomap  23674  qtopcmap  23675  kqffn  23681  hmeof1o2  23719  xkocnv  23770  rnelfm  23909  ptcmplem1  24008  cnextfres1  24024  ghmcnp  24071  tgphaus  24073  prdstmdd  24080  prdstgpd  24081  fmucnd  24247  psmetxrge0  24269  isxmet2d  24283  prdsmet  24326  blelrnps  24372  blelrn  24373  xmetresbl  24393  comet  24469  stdbdxmet  24471  met2ndci  24478  prdsxmslem2  24485  isngp3  24554  nmotri  24695  metdsre  24810  bndth  24925  evth  24926  fmcfil  25240  bcthlem4  25295  rrxcph  25360  rrxds  25361  rrxmet  25376  evthicc2  25429  ovolfsf  25440  ovolmge0  25446  ovollb2lem  25457  ovolunlem1a  25465  ovoliunlem1  25471  ovoliun  25474  ovoliun2  25475  ovolscalem1  25482  ovolicc1  25485  ovolicc2lem4  25489  ovolicc2  25491  voliunlem1  25519  voliunlem3  25521  volsup  25525  ioombl1lem2  25528  ioombl1lem4  25530  uniiccdif  25547  uniioombllem2  25552  uniioombllem3  25554  uniioombllem6  25557  volsup2  25574  vitalilem4  25580  mbfeqalem1  25610  mbfmulc2lem  25616  mbfmax  25618  mbfaddlem  25629  mbfadd  25630  mbfsub  25631  mbfsup  25633  mbfinf  25634  itg1ge0  25655  itg1addlem1  25661  i1faddlem  25662  i1fmullem  25663  i1fadd  25664  i1fmul  25665  itg1addlem4  25668  i1fmulclem  25671  i1fmulc  25672  itg1mulc  25673  i1fres  25674  itg10a  25679  itg1ge0a  25680  itg1lea  25681  mbfi1fseqlem3  25686  mbfi1fseqlem4  25687  mbfi1flimlem  25691  mbfmullem2  25693  mbfmul  25695  itg20  25706  itg2lea  25713  itg2splitlem  25717  itg2split  25718  itg2monolem1  25719  itg2monolem2  25720  itg2monolem3  25721  itg2mono  25722  itg2i1fseqle  25723  itg2i1fseq  25724  itg2addlem  25727  itg2gt0  25729  itg2cnlem1  25730  itg2cnlem2  25731  itg2cn  25732  itgitg1  25778  bddmulibl  25808  bddibl  25809  dvidlem  25884  dvaddbr  25908  dvmulbr  25909  dvmulbrOLD  25910  dvaddf  25913  dvcmulf  25916  dvrec  25927  dvcnvlem  25948  rolle  25962  dveq0  25973  dv11cn  25974  dvivthlem2  25982  dvivth  25983  dvne0  25984  lhop1lem  25986  lhop1  25987  lhop2  25988  lhop  25989  ftc1cn  26018  tdeglem1  26031  tdeglem3  26032  tdeglem4  26033  mdegleb  26037  mdegldg  26039  mdegaddle  26047  ply1remlem  26138  ply1rem  26139  fta1glem1  26141  fta1glem2  26142  fta1blem  26144  idomrootle  26146  plyeq0lem  26183  plyeq0  26184  plyaddlem1  26186  coeeulem  26197  coeaddlem  26222  coemulc  26228  dgradd2  26242  dgrcolem2  26248  ofmulrt  26257  plyrem  26281  vieta1lem1  26286  vieta1  26288  plyexmo  26289  elqaalem3  26297  aannenlem1  26304  aalioulem2  26309  ulmuni  26369  ulmdvlem1  26377  ulmdv  26380  mbfulm  26383  iblulm  26384  itgulm  26385  rlimcnp2  26944  jensen  26967  amgm  26969  basellem3  27061  basellem7  27065  basellem9  27067  dchrelbas2  27216  dchrmulcl  27228  dchrfi  27234  dchreq  27237  dchrresb  27238  dchrinv  27240  dchr1re  27242  sumdchr2  27249  dchr2sum  27252  lgsqrlem2  27326  lgsqrlem3  27327  rpvmasum2  27491  dchrisum0re  27492  mirf1o  28753  lmif1o  28879  eqeefv  28988  axlowdimlem14  29040  vtxdgfisf  29562  2pthon3v  30028  nvinvfval  30727  sspg  30815  ssps  30817  sspmlem  30819  sspn  30823  lnon0  30885  ubthlem1  30957  pjfn  31796  kbpj  32043  kbass2  32204  elpjrn  32277  ofrn2  32729  off2  32730  ofresid  32731  xppreima2  32740  ofpreima2  32755  suppovss  32770  resf1o  32819  prodindf  32954  indpreima  32957  swrdrn3  33047  pwrssmgc  33092  mgcf1o  33095  gsumfs2d  33154  gsumhashmul  33160  symgcom2  33177  pmtrcnel  33182  pmtrcnel2  33183  pmtrcnelor  33184  cycpmfvlem  33205  cycpmfv3  33208  cycpmcl  33209  cycpmco2rn  33218  cycpmco2  33226  cycpm3cl2  33229  cyc3co2  33233  cyc3evpm  33243  elrgspnlem1  33335  elrgspnlem2  33336  elrgspnlem4  33338  elrgspnsubrunlem1  33340  elrgspnsubrunlem2  33341  gsumind  33437  islinds5  33459  ellspds  33460  elrspunidl  33520  elrspunsn  33521  rhmimaidl  33524  rhmpreimaprmidl  33543  rprmdvdsprod  33626  1arithidomlem2  33628  evls1fn  33652  ply1dg1rt  33672  ply1mulrtss  33674  ply1degltel  33686  ply1degleel  33687  ply1degltlss  33688  ply1gsumz  33691  ig1pmindeg  33694  r1pquslmic  33703  extvfvcl  33712  mplmulmvr  33715  evlextv  33718  mplvrpmmhm  33722  mplvrpmrhm  33723  psrmonprod  33728  esplyfval0  33740  esplyfval2  33741  esplyfv1  33745  esplyfv  33746  esplyfval3  33748  esplyfvaln  33750  esplyind  33751  vieta  33756  exsslsb  33773  ply1degltdimlem  33799  ply1degltdim  33800  dimkerim  33804  fedgmullem2  33807  fedgmul  33808  lvecendof1f1o  33810  fldextrspunlsplem  33850  fldextrspunlsp  33851  irngss  33864  irngnzply1  33868  extdgfialglem2  33870  irngnminplynz  33889  2sqr3minply  33957  cos9thpiminply  33965  cmpcref  34027  rhmpreimacnlem  34061  fsumcvg4  34127  pl1cn  34132  qqhval2lem  34158  esumcvg  34263  ofcf  34280  ofcof  34284  measfn  34381  meascnbl  34396  sibfof  34517  sitgaddlemb  34525  subiwrdlen  34563  rrvfn  34622  plymul02  34723  signsplypnf  34727  signsply0  34728  reprsuc  34792  reprdifc  34804  breprexplema  34807  circlemethhgt  34820  hgt750lemb  34833  f1resrcmplf1dlem  35261  pthhashvtx  35341  cvmopnlem  35491  cvmliftmolem1  35494  cvmliftlem10  35507  cvmlift2lem9a  35516  cvmlift2lem6  35521  cvmlift2lem12  35527  cvmliftphtlem  35530  cvmlift3lem9  35540  mrsubrn  35726  elmrsubrn  35733  elmsubrn  35741  msubrn  35742  mclsind  35783  mclsppslem  35796  mclspps  35797  iprodefisumlem  35953  weiunfrlem  36677  matunitlindflem1  37864  poimirlem1  37869  poimirlem2  37870  poimirlem3  37871  poimirlem16  37884  poimirlem17  37885  poimirlem19  37887  poimirlem20  37888  poimirlem22  37890  poimirlem23  37891  poimirlem29  37897  poimirlem30  37898  poimirlem31  37899  poimir  37901  mblfinlem2  37906  itg2addnclem3  37921  itg2addnc  37922  itg2gt0cn  37923  ftc1cnnc  37940  ftc1anclem5  37945  ftc1anclem7  37947  ftc1anc  37949  sdclem2  37990  istotbnd3  38019  sstotbnd2  38022  isbnd3  38032  heibor1lem  38057  rrnmet  38077  grpokerinj  38141  isdrngo2  38206  lfl1  39443  lfladdcl  39444  lflvscl  39450  lkr0f  39467  lkrsc  39470  eqlkr2  39473  eqlkr3  39474  ldualvaddval  39504  ldualvsval  39511  tendoeq1  41137  zndvdchrrhm  42339  hashscontpow  42489  aks6d1c3  42490  aks6d1c2lem4  42494  aks6d1c2  42497  sticksstones1  42513  sticksstones2  42514  sticksstones3  42515  sticksstones12a  42524  sticksstones12  42525  aks6d1c6lem2  42538  aks6d1c6lem3  42539  aks6d1c6isolem1  42541  aks6d1c6isolem3  42543  aks6d1c6lem5  42544  aks6d1c7lem1  42547  unitscyglem1  42562  dvun  42726  frlmvscadiccat  42873  fiabv  42903  frlmsnic  42907  mplmapghm  42919  evlsaddval  42926  evlsmulval  42927  selvvvval  42940  evlselvlem  42941  evlselv  42942  fsuppssind  42948  mhphf  42952  ismrcd1  43052  ismrcd2  43053  istopclsd  43054  isnacs3  43064  mzpaddmpt  43095  mzpmulmpt  43096  mzpsubst  43102  mzpcong  43326  fnwe2lem2  43405  islmodfg  43423  kercvrlsm  43437  dgrsub2  43489  mpaaeu  43504  rngunsnply  43523  hausgraph  43559  ofoafg  43708  ofoafo  43710  ofoaid1  43712  ofoaid2  43713  naddcnff  43716  naddcnffn  43717  naddcnffo  43718  naddcnfcom  43720  naddcnfid1  43721  naddcnfass  43723  fsovf1od  44369  brcoffn  44383  clsneiel1  44461  wfximgfd  44516  extoimad  44517  mnringmulrcld  44581  mnurndlem1  44634  caofcan  44676  ofmul12  44678  ofdivrec  44679  ofdivcan4  44680  ofdivdiv2  44681  dvconstbi  44687  binomcxplemnotnn0  44709  relpmin  45305  refsum2cnlem1  45394  ssmapsn  45571  preimaiocmnf  45917  fsumsupp0  45935  fsumsermpt  45936  climinf  45963  climinf2lem  46061  limsupmnflem  46075  limsupvaluz2  46093  supcnvlimsup  46095  limsupgtlem  46132  liminfvalxr  46138  liminflelimsupuz  46140  xlimconst2  46190  climxlim2  46201  icccncfext  46242  dvnprodlem1  46301  volicoff  46350  voliooicof  46351  fourierdlem25  46487  etransclem2  46591  etransclem35  46624  fge0iccico  46725  sge0tsms  46735  sge0sup  46746  sge0resrn  46759  sge0le  46762  sge0fodjrnlem  46771  sge0isum  46782  sge0seq  46801  nnfoctbdjlem  46810  meadjiunlem  46820  omeiunle  46872  hoicvr  46903  ovolval4lem1  47004  ovolval5lem3  47009  ovnovollem1  47011  ovnovollem2  47012  iinhoiicclem  47028  iunhoiioolem  47030  preimaicomnf  47066  smfresal  47143  smfsuplem1  47166  smflimsuplem2  47176  fcoreslem3  47422  fcoreslem4  47423  fcores  47424  isubgredg  48223  upgrimpths  48266  ackvalsucsucval  49045  funchomf  49453  imasubc  49507  imassc  49509  imaid  49510  prcofdiag1  49749  prcofdiag  49750  oppfdiag1  49770  oppfdiag  49772  amgmwlem  50158