Theorem ffnd 6737

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

Syntax hints:   → wi 4   Fn wfn 6557  ⟶wf 6558

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 6566

This theorem is referenced by:  fnconstg  6796  f1fn  6805  fofn  6822  f1ofn  6849  feqmptd  6976  fssrescdmd  7145  fprb  7213  cocan1  7310  oprres  7600  off  7714  coof  7720  ofco  7721  caofref  7727  caofid0l  7729  caofid0r  7730  caofid1  7731  caofid2  7732  caofrss  7734  caoftrn  7736  fo2ndf  8144  fnwelem  8154  fnse  8156  suppsnop  8201  suppss  8217  suppssr  8218  suppssrg  8219  suppssof1  8222  suppofssd  8226  suppofss1d  8227  suppofss2d  8228  suppcoss  8230  smocdmdom  8406  elmapfn  8903  ralxpmap  8934  omxpenlem  9111  mapen  9179  f1finf1o  9302  f1finf1oOLD  9303  unirnffid  9384  fdmfifsupp  9412  mapfien  9445  intrnfi  9453  marypha2  9476  ordtypelem7  9561  wemapsolem  9587  wemapso  9588  wemapso2lem  9589  unxpwdom2  9625  ixpiunwdom  9627  cantnfle  9708  cantnfp1lem2  9716  cantnfp1lem3  9717  cantnfp1  9718  oemapvali  9721  cantnflem1a  9722  cantnflem1c  9724  cantnflem3  9728  cantnf  9730  cnfcomlem  9736  cnfcom3  9741  updjudhcoinlf  9969  updjudhcoinrg  9970  fseqenlem1  10061  numacn  10086  infpwfien  10099  isf32lem2  10391  isf34lem7  10416  isf34lem6  10417  unirnfdomd  10604  ofsubeq0  12260  ofnegsub  12261  ofsubge0  12262  seqf1olem2  14079  resunimafz0  14480  wrdfn  14562  swrdvalfn  14685  pfxfn  14715  pfxid  14718  cats1un  14755  cshwfn  14835  ccatco  14870  limsupgle  15509  o1of2  15645  o1rlimmul  15651  isercolllem2  15698  isercoll  15700  isercoll2  15701  climsup  15702  fsumss  15757  ruclem11  16272  vdwlem2  17015  vdwlem6  17019  vdwlem9  17022  vdwlem12  17025  0ram  17053  ramub1lem1  17059  pwsle  17538  pwsleval  17539  pwsvscaval  17541  mrcuni  17665  mrcun  17666  invf1o  17816  funcres2c  17954  setcmon  18140  setcepi  18141  uncfcurf  18295  yoniso  18341  isacs4lem  18601  acsmapd  18611  gsumval2  18711  mgmhmf1o  18725  resmgmhm2b  18738  mgmhmima  18740  mgmhmeql  18741  prdsplusgsgrpcl  18757  prdssgrpd  18758  prdsplusgcl  18793  prdsidlem  18794  prdsmndd  18795  mhmf1o  18821  resmhm2b  18847  mhmimalem  18849  mhmima  18850  mhmeql  18851  prdspjmhm  18854  pwsco1mhm  18857  pwsco2mhm  18858  gsumwmhm  18870  frmdss2  18888  grpinvf1o  19039  prdsinvlem  19079  cycsubgcl  19236  ghmrn  19259  ghmpreima  19268  ghmeql  19269  ghmnsgima  19270  ghmnsgpreima  19271  ghmeqker  19273  ghmf1o  19278  ghmqusnsglem1  19310  ghmqusnsg  19312  ghmquskerlem1  19313  ghmquskerco  19314  ghmquskerlem3  19316  ghmqusker  19317  gass  19331  cntzmhm  19371  symgextres  19457  gsmsymgrfixlem1  19459  fvcosymgeq  19461  f1omvdconj  19478  pmtrfinv  19493  symgtrinv  19504  pmtr3ncomlem1  19505  sygbasnfpfi  19544  efginvrel2  19759  efgredleme  19775  ghmplusg  19878  prdscmnd  19893  gsumval3a  19935  gsumval3eu  19936  gsumzaddlem  19953  gsumzsplit  19959  gsumpt  19994  prdsgsum  20013  dprdfcntz  20049  dprdfadd  20054  dprdfeq0  20056  dprdf11  20057  dprdlub  20060  dprdspan  20061  dprd2dlem1  20075  dmdprdpr  20083  dprdpr  20084  dpjlem  20085  ablfac1eu  20107  prdsmulrngcl  20192  prdsrngd  20193  prdsringd  20334  prdscrngd  20335  prds1  20336  pwspjmhmmgpd  20341  rnghmf1o  20468  rhmf1o  20507  rhmimasubrnglem  20581  rnrhmsubrg  20621  rrgsupp  20717  imadrhmcl  20814  isabvd  20829  lmodfopnelem1  20912  lcomfsupp  20916  prdsvscacl  20983  prdslmodd  20984  lmhmco  21059  lmhmplusg  21060  lmhmvsca  21061  lmhmf1o  21062  lmhmeql  21071  lspextmo  21072  rhmpreimaidl  21304  pjfo  21752  dsmmbas2  21774  dsmm0cl  21777  dsmmacl  21778  dsmmsubg  21780  dsmmlss  21781  frlmvplusgvalc  21804  frlmvscaval  21805  frlmplusgvalb  21806  frlmvscavalb  21807  frlmsslss2  21812  frlmphllem  21817  frlmphl  21818  frlmssuvc2  21832  frlmsslsp  21833  frlmup1  21835  frlmup2  21836  frlmup3  21837  frlmup4  21838  islindf4  21875  psrbagfsupp  21956  psrbaglesupp  21959  psrbaglecl  21960  psrbagaddcl  21961  psrbagcon  21962  psrbaglefi  21963  psrbagleadd1  21965  psrbagconf1o  21966  gsumbagdiaglem  21967  psrass1lem  21969  psrvscaval  21987  psrlidm  21999  psrridm  22000  psrass1  22001  psrdi  22002  psrdir  22003  psrascl  22016  mvrf2  22030  mplsubglem  22036  mplvscaval  22053  subrgmvrf  22069  mplbas2  22077  mplind  22111  psrbagev1  22118  psrbagev2  22119  evlslem3  22121  evlslem1  22123  evlsvar  22131  mpfind  22148  ismhp3  22163  mhpmulcl  22170  psdmplcl  22183  psdadd  22184  psdvsca  22185  psdmul  22187  psrplusgpropd  22252  coe1add  22282  coe1addfv  22283  evl1addd  22360  evl1subd  22361  evl1muld  22362  pf1mpf  22371  pf1ind  22374  evls1fpws  22388  ressply1evl  22389  rhmply1vsca  22407  mamudir  22423  mamulid  22462  mamurid  22463  mdetrlin  22623  mdetrsca  22624  mdetralt  22629  mdetunilem7  22639  mdetunilem9  22641  madurid  22665  cnrest2  23309  lmss  23321  lmcnp  23327  cnt0  23369  cnt1  23373  cnhaus  23377  rncmp  23419  conncn  23449  2ndcomap  23481  1stccnp  23485  comppfsc  23555  1stckgenlem  23576  ptbasfi  23604  ptopn  23606  ptclsg  23638  ptcnp  23645  upxp  23646  txtube  23663  txcmplem1  23664  hauseqlcld  23669  xkohaus  23676  xkoptsub  23677  cnmpt11  23686  cnmpt21  23694  cnmpt22f  23698  cnmptcom  23701  qtopss  23738  qtopeu  23739  qtopomap  23741  qtopcmap  23742  kqffn  23748  hmeof1o2  23786  xkocnv  23837  rnelfm  23976  ptcmplem1  24075  cnextfres1  24091  ghmcnp  24138  tgphaus  24140  prdstmdd  24147  prdstgpd  24148  fmucnd  24316  psmetxrge0  24338  isxmet2d  24352  prdsmet  24395  blelrnps  24441  blelrn  24442  xmetresbl  24462  comet  24541  stdbdxmet  24543  met2ndci  24550  prdsxmslem2  24557  isngp3  24626  nmotri  24775  metdsre  24888  bndth  25003  evth  25004  fmcfil  25319  bcthlem4  25374  rrxcph  25439  rrxds  25440  rrxmet  25455  evthicc2  25508  ovolfsf  25519  ovolmge0  25525  ovollb2lem  25536  ovolunlem1a  25544  ovoliunlem1  25550  ovoliun  25553  ovoliun2  25554  ovolscalem1  25561  ovolicc1  25564  ovolicc2lem4  25568  ovolicc2  25570  voliunlem1  25598  voliunlem3  25600  volsup  25604  ioombl1lem2  25607  ioombl1lem4  25609  uniiccdif  25626  uniioombllem2  25631  uniioombllem3  25633  uniioombllem6  25636  volsup2  25653  vitalilem4  25659  mbfeqalem1  25689  mbfmulc2lem  25695  mbfmax  25697  mbfaddlem  25708  mbfadd  25709  mbfsub  25710  mbfsup  25712  mbfinf  25713  itg1ge0  25734  itg1addlem1  25740  i1faddlem  25741  i1fmullem  25742  i1fadd  25743  i1fmul  25744  itg1addlem4  25747  itg1addlem4OLD  25748  i1fmulclem  25751  i1fmulc  25752  itg1mulc  25753  i1fres  25754  itg10a  25759  itg1ge0a  25760  itg1lea  25761  mbfi1fseqlem3  25766  mbfi1fseqlem4  25767  mbfi1flimlem  25771  mbfmullem2  25773  mbfmul  25775  itg20  25786  itg2lea  25793  itg2splitlem  25797  itg2split  25798  itg2monolem1  25799  itg2monolem2  25800  itg2monolem3  25801  itg2mono  25802  itg2i1fseqle  25803  itg2i1fseq  25804  itg2addlem  25807  itg2gt0  25809  itg2cnlem1  25810  itg2cnlem2  25811  itg2cn  25812  itgitg1  25858  bddmulibl  25888  bddibl  25889  dvidlem  25964  dvaddbr  25988  dvmulbr  25989  dvmulbrOLD  25990  dvaddf  25993  dvcmulf  25996  dvrec  26007  dvcnvlem  26028  rolle  26042  dveq0  26053  dv11cn  26054  dvivthlem2  26062  dvivth  26063  dvne0  26064  lhop1lem  26066  lhop1  26067  lhop2  26068  lhop  26069  ftc1cn  26098  tdeglem1  26111  tdeglem3  26112  tdeglem4  26113  mdegleb  26117  mdegldg  26119  mdegaddle  26127  ply1remlem  26218  ply1rem  26219  fta1glem1  26221  fta1glem2  26222  fta1blem  26224  idomrootle  26226  plyeq0lem  26263  plyeq0  26264  plyaddlem1  26266  coeeulem  26277  coeaddlem  26302  coemulc  26308  dgradd2  26322  dgrcolem2  26328  ofmulrt  26337  plyrem  26361  vieta1lem1  26366  vieta1  26368  plyexmo  26369  elqaalem3  26377  aannenlem1  26384  aalioulem2  26389  ulmuni  26449  ulmdvlem1  26457  ulmdv  26460  mbfulm  26463  iblulm  26464  itgulm  26465  rlimcnp2  27023  jensen  27046  amgm  27048  basellem3  27140  basellem7  27144  basellem9  27146  dchrelbas2  27295  dchrmulcl  27307  dchrfi  27313  dchreq  27316  dchrresb  27317  dchrinv  27319  dchr1re  27321  sumdchr2  27328  dchr2sum  27331  lgsqrlem2  27405  lgsqrlem3  27406  rpvmasum2  27570  dchrisum0re  27571  mirf1o  28691  lmif1o  28817  eqeefv  28932  axlowdimlem14  28984  vtxdgfisf  29508  2pthon3v  29972  nvinvfval  30668  sspg  30756  ssps  30758  sspmlem  30760  sspn  30764  lnon0  30826  ubthlem1  30898  pjfn  31737  kbpj  31984  kbass2  32145  elpjrn  32218  ofrn2  32656  off2  32657  ofresid  32658  xppreima2  32667  ofpreima2  32682  suppovss  32695  resf1o  32747  swrdrn3  32924  pwrssmgc  32974  mgcf1o  32977  chnso  32987  gsumfs2d  33040  gsumhashmul  33046  gsumle  33083  symgcom2  33086  pmtrcnel  33091  pmtrcnel2  33092  pmtrcnelor  33093  cycpmfvlem  33114  cycpmfv3  33117  cycpmcl  33118  cycpmco2rn  33127  cycpmco2  33135  cycpm3cl2  33138  cyc3co2  33142  cyc3evpm  33152  elrgspnlem1  33231  elrgspnlem2  33232  elrgspnlem4  33234  islinds5  33374  ellspds  33375  elrspunidl  33435  elrspunsn  33436  rhmimaidl  33439  rhmpreimaprmidl  33458  rprmdvdsprod  33541  1arithidomlem2  33543  evls1fn  33565  ply1dg1rt  33583  ply1mulrtss  33585  ply1degltel  33594  ply1degleel  33595  ply1degltlss  33596  ply1gsumz  33598  ig1pmindeg  33601  r1pquslmic  33610  ply1degltdimlem  33649  ply1degltdim  33650  dimkerim  33654  fedgmullem2  33657  fedgmul  33658  lvecendof1f1o  33660  irngss  33701  irngnzply1  33705  irngnminplynz  33719  2sqr3minply  33752  cmpcref  33810  rhmpreimacnlem  33844  fsumcvg4  33910  pl1cn  33915  qqhval2lem  33943  prodindf  34003  indpreima  34005  esumcvg  34066  ofcf  34083  ofcof  34087  measfn  34184  meascnbl  34199  sibfof  34321  sitgaddlemb  34329  subiwrdlen  34367  rrvfn  34426  plymul02  34539  signsplypnf  34543  signsply0  34544  reprsuc  34608  reprdifc  34620  breprexplema  34623  circlemethhgt  34636  hgt750lemb  34649  f1resrcmplf1dlem  35078  pthhashvtx  35111  cvmopnlem  35262  cvmliftmolem1  35265  cvmliftlem10  35278  cvmlift2lem9a  35287  cvmlift2lem6  35292  cvmlift2lem12  35298  cvmliftphtlem  35301  cvmlift3lem9  35311  mrsubrn  35497  elmrsubrn  35504  elmsubrn  35512  msubrn  35513  mclsind  35554  mclsppslem  35567  mclspps  35568  iprodefisumlem  35719  weiunfrlem  36446  matunitlindflem1  37602  poimirlem1  37607  poimirlem2  37608  poimirlem3  37609  poimirlem16  37622  poimirlem17  37623  poimirlem19  37625  poimirlem20  37626  poimirlem22  37628  poimirlem23  37629  poimirlem29  37635  poimirlem30  37636  poimirlem31  37637  poimir  37639  mblfinlem2  37644  itg2addnclem3  37659  itg2addnc  37660  itg2gt0cn  37661  ftc1cnnc  37678  ftc1anclem5  37683  ftc1anclem7  37685  ftc1anc  37687  sdclem2  37728  istotbnd3  37757  sstotbnd2  37760  isbnd3  37770  heibor1lem  37795  rrnmet  37815  grpokerinj  37879  isdrngo2  37944  lfl1  39051  lfladdcl  39052  lflvscl  39058  lkr0f  39075  lkrsc  39078  eqlkr2  39081  eqlkr3  39082  ldualvaddval  39112  ldualvsval  39119  tendoeq1  40746  zndvdchrrhm  41952  hashscontpow  42103  aks6d1c3  42104  aks6d1c2lem4  42108  aks6d1c2  42111  sticksstones1  42127  sticksstones2  42128  sticksstones3  42129  sticksstones12a  42138  sticksstones12  42139  aks6d1c6lem2  42152  aks6d1c6lem3  42153  aks6d1c6isolem1  42155  aks6d1c6isolem3  42157  aks6d1c6lem5  42158  aks6d1c7lem1  42161  unitscyglem1  42176  metakunt19  42204  metakunt25  42210  metakunt33  42218  dvun  42367  frlmvscadiccat  42492  fiabv  42522  frlmsnic  42526  pwsgprod  42530  mplmapghm  42542  evlsvvval  42549  evlsaddval  42554  evlsmulval  42555  evladdval  42561  evlmulval  42562  selvvvval  42571  evlselvlem  42572  evlselv  42573  fsuppssind  42579  mhphf  42583  ismrcd1  42685  ismrcd2  42686  istopclsd  42687  isnacs3  42697  mzpaddmpt  42728  mzpmulmpt  42729  mzpsubst  42735  mzpcong  42960  fnwe2lem2  43039  islmodfg  43057  kercvrlsm  43071  dgrsub2  43123  mpaaeu  43138  rngunsnply  43157  hausgraph  43193  ofoafg  43343  ofoafo  43345  ofoaid1  43347  ofoaid2  43348  naddcnff  43351  naddcnffn  43352  naddcnffo  43353  naddcnfcom  43355  naddcnfid1  43356  naddcnfass  43358  fsovf1od  44005  brcoffn  44019  clsneiel1  44097  wfximgfd  44152  extoimad  44153  mnringmulrcld  44223  mnurndlem1  44276  caofcan  44318  ofmul12  44320  ofdivrec  44321  ofdivcan4  44322  ofdivdiv2  44323  dvconstbi  44329  binomcxplemnotnn0  44351  refsum2cnlem1  44974  ssmapsn  45158  preimaiocmnf  45513  fsumsupp0  45533  fsumsermpt  45534  climinf  45561  climinf2lem  45661  limsupmnflem  45675  limsupvaluz2  45693  supcnvlimsup  45695  limsupgtlem  45732  liminfvalxr  45738  liminflelimsupuz  45740  xlimconst2  45790  climxlim2  45801  icccncfext  45842  dvnprodlem1  45901  volicoff  45950  voliooicof  45951  fourierdlem25  46087  etransclem2  46191  etransclem35  46224  fge0iccico  46325  sge0tsms  46335  sge0sup  46346  sge0resrn  46359  sge0le  46362  sge0fodjrnlem  46371  sge0isum  46382  sge0seq  46401  nnfoctbdjlem  46410  meadjiunlem  46420  omeiunle  46472  hoicvr  46503  ovolval4lem1  46604  ovolval5lem3  46609  ovnovollem1  46611  ovnovollem2  46612  iinhoiicclem  46628  iunhoiioolem  46630  preimaicomnf  46666  smfresal  46743  smfsuplem1  46766  smflimsuplem2  46776  fcoreslem3  47014  fcoreslem4  47015  fcores  47016  isubgredg  47789  ackvalsucsucval  48537  amgmwlem  49032