Theorem ffnd 6696

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

Syntax hints:   → wi 4   Fn wfn 6520  ⟶wf 6521

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 210  df-an 401  df-f 6529

This theorem is referenced by:  fnconstg  6756  f1fn  6765  fofn  6784  f1ofn  6811  feqmptd  6939  fssrescdmd  7112  fprb  7182  cocan1  7279  oprres  7568  off  7682  coof  7688  ofco  7689  caofref  7695  caofid0l  7697  caofid0r  7698  caofid1  7699  caofid2  7700  caofrss  7703  caoftrn  7705  fo2ndf  8104  fnwelem  8115  fnse  8117  suppsnop  8162  suppss  8178  suppssr  8179  suppssrg  8180  suppssof1  8183  suppofssd  8187  suppofss1d  8188  suppofss2d  8189  suppcoss  8191  smocdmdom  8343  elmapfn  8850  ralxpmap  8882  omxpenlem  9054  mapen  9117  f1finf1o  9221  unirnffid  9292  fdmfifsupp  9323  mapfien  9356  intrnfi  9364  marypha2  9387  ordtypelem7  9474  wemapsolem  9500  wemapso  9501  wemapso2lem  9502  unxpwdom2  9538  ixpiunwdom  9540  cantnfle  9628  cantnfp1lem2  9636  cantnfp1lem3  9637  cantnfp1  9638  oemapvali  9641  cantnflem1a  9642  cantnflem1c  9644  cantnflem3  9648  cantnf  9650  cnfcomlem  9656  cnfcom3  9661  updjudhcoinlf  9906  updjudhcoinrg  9907  fseqenlem1  9996  numacn  10021  infpwfien  10034  isf32lem2  10326  isf34lem7  10351  isf34lem6  10352  unirnfdomd  10540  ofsubeq0  12203  ofnegsub  12204  ofsubge0  12205  seqf1olem2  14066  resunimafz0  14470  wrdfn  14553  swrdvalfn  14677  pfxfn  14707  pfxid  14710  cats1un  14746  cshwfn  14826  ccatco  14860  limsupgle  15516  o1of2  15652  o1rlimmul  15658  isercolllem2  15705  isercoll  15707  isercoll2  15708  climsup  15709  fsumss  15764  ruclem11  16284  vdwlem2  17030  vdwlem6  17034  vdwlem9  17037  vdwlem12  17040  0ram  17068  ramub1lem1  17074  pwsle  17534  pwsleval  17535  pwsvscaval  17537  mrcuni  17665  mrcun  17666  invf1o  17814  funcres2c  17948  setcmon  18132  setcepi  18133  uncfcurf  18283  yoniso  18329  isacs4lem  18588  acsmapd  18598  chnso  18668  gsumval2  18732  mgmhmf1o  18746  resmgmhm2b  18759  mgmhmima  18761  mgmhmeql  18762  prdsplusgsgrpcl  18778  prdssgrpd  18779  prdsplusgcl  18814  prdsidlem  18815  prdsmndd  18816  mhmf1o  18842  resmhm2b  18869  mhmimalem  18871  mhmima  18872  mhmeql  18873  prdspjmhm  18876  pwsco1mhm  18879  pwsco2mhm  18880  gsumwmhm  18892  frmdss2  18910  grpinvf1o  19063  prdsinvlem  19103  cycsubgcl  19265  ghmrn  19287  ghmpreima  19296  ghmeql  19297  ghmnsgima  19298  ghmnsgpreima  19299  ghmeqker  19301  ghmf1o  19306  ghmqusnsglem1  19338  ghmqusnsg  19340  ghmquskerlem1  19341  ghmquskerco  19342  ghmquskerlem3  19344  ghmqusker  19345  gass  19359  cntzmhm  19399  symgextres  19483  gsmsymgrfixlem1  19485  fvcosymgeq  19487  f1omvdconj  19504  pmtrfinv  19519  symgtrinv  19530  pmtr3ncomlem1  19531  sygbasnfpfi  19570  efginvrel2  19785  efgredleme  19801  ghmplusg  19904  prdscmnd  19919  gsumval3a  19961  gsumval3eu  19962  gsumzaddlem  19979  gsumzsplit  19985  gsumpt  20020  prdsgsum  20039  dprdfcntz  20075  dprdfadd  20080  dprdfeq0  20082  dprdf11  20083  dprdlub  20086  dprdspan  20087  dprd2dlem1  20101  dmdprdpr  20109  dprdpr  20110  dpjlem  20111  ablfac1eu  20133  gsumle  20203  prdsmulrngcl  20241  prdsrngd  20242  prdsringd  20390  prdscrngd  20391  prds1  20392  pwspjmhmmgpd  20397  pwsgprod  20399  rnghmf1o  20522  rhmf1o  20561  rhmimasubrnglem  20638  rnrhmsubrg  20678  rrgsupp  20774  imadrhmcl  20866  isabvd  20881  lmodfopnelem1  20985  lcomfsupp  20989  prdsvscacl  21055  prdslmodd  21056  lmhmco  21130  lmhmplusg  21131  lmhmvsca  21132  lmhmf1o  21133  lmhmeql  21142  lspextmo  21143  rhmpreimaidl  21375  rhmpreimaprmidl  21436  pjfo  21822  dsmmbas2  21844  dsmm0cl  21847  dsmmacl  21848  dsmmsubg  21850  dsmmlss  21851  frlmvplusgvalc  21874  frlmvscaval  21875  frlmplusgvalb  21876  frlmvscavalb  21877  frlmsslss2  21882  frlmphllem  21887  frlmphl  21888  frlmssuvc2  21902  frlmsslsp  21903  frlmup1  21905  frlmup2  21906  frlmup3  21907  frlmup4  21908  islindf4  21945  psrbagfsupp  22026  psrbaglesupp  22029  psrbaglecl  22030  psrbagaddcl  22031  psrbagcon  22032  psrbaglefi  22033  psrbagleadd1  22035  psrbagconf1o  22036  gsumbagdiaglem  22038  psrass1lem  22040  psrvscaval  22057  psrlidm  22068  psrridm  22069  psrass1  22070  psrdi  22071  psrdir  22072  psrascl  22085  mvrf2  22099  mplsubglem  22105  mplvscaval  22122  subrgmvrf  22142  mplbas2  22150  mplind  22178  psrbagev1  22185  psrbagev2  22186  evlslem3  22188  evlslem1  22190  evlsvvval  22201  evlsvar  22203  evladdval  22211  evlmulval  22212  mpfind  22223  mplmapghm  22230  evlsaddval  22237  evlsmulval  22238  selvvvval  22250  ismhp3  22262  mhpmulcl  22269  psdmplcl  22282  psdadd  22283  psdvsca  22284  psdmul  22286  psdmvr  22289  psrplusgpropd  22352  coe1add  22382  coe1addfv  22383  evl1addd  22458  evl1subd  22459  evl1muld  22460  pf1mpf  22469  pf1ind  22472  evls1fpws  22486  ressply1evl  22487  rhmply1vsca  22502  mamudir  22518  mamulid  22555  mamurid  22556  mdetrlin  22716  mdetrsca  22717  mdetralt  22722  mdetunilem7  22732  mdetunilem9  22734  madurid  22758  cnrest2  23400  lmss  23412  lmcnp  23418  cnt0  23460  cnt1  23464  cnhaus  23468  rncmp  23510  conncn  23540  2ndcomap  23572  1stccnp  23576  comppfsc  23646  1stckgenlem  23667  ptbasfi  23695  ptopn  23697  ptclsg  23729  ptcnp  23736  upxp  23737  txtube  23754  txcmplem1  23755  hauseqlcld  23760  xkohaus  23767  xkoptsub  23768  cnmpt11  23777  cnmpt21  23785  cnmpt22f  23789  cnmptcom  23792  qtopss  23829  qtopeu  23830  qtopomap  23832  qtopcmap  23833  kqffn  23839  hmeof1o2  23877  xkocnv  23928  rnelfm  24067  ptcmplem1  24166  cnextfres1  24182  ghmcnp  24229  tgphaus  24231  prdstmdd  24238  prdstgpd  24239  fmucnd  24405  psmetxrge0  24427  isxmet2d  24441  prdsmet  24484  blelrnps  24530  blelrn  24531  xmetresbl  24551  comet  24627  stdbdxmet  24629  met2ndci  24636  prdsxmslem2  24643  isngp3  24712  nmotri  24853  metdsre  24968  bndth  25074  evth  25075  fmcfil  25388  bcthlem4  25443  rrxcph  25508  rrxds  25509  rrxmet  25524  evthicc2  25576  ovolfsf  25587  ovolmge0  25593  ovollb2lem  25604  ovolunlem1a  25612  ovoliunlem1  25618  ovoliun  25621  ovoliun2  25622  ovolscalem1  25629  ovolicc1  25632  ovolicc2lem4  25636  ovolicc2  25638  voliunlem1  25666  voliunlem3  25668  volsup  25672  ioombl1lem2  25675  ioombl1lem4  25677  uniiccdif  25694  uniioombllem2  25699  uniioombllem3  25701  uniioombllem6  25704  volsup2  25721  vitalilem4  25727  mbfeqalem1  25757  mbfmulc2lem  25763  mbfmax  25765  mbfaddlem  25776  mbfadd  25777  mbfsub  25778  mbfsup  25780  mbfinf  25781  itg1ge0  25802  itg1addlem1  25808  i1faddlem  25809  i1fmullem  25810  i1fadd  25811  i1fmul  25812  itg1addlem4  25815  i1fmulclem  25818  i1fmulc  25819  itg1mulc  25820  i1fres  25821  itg10a  25826  itg1ge0a  25827  itg1lea  25828  mbfi1fseqlem3  25833  mbfi1fseqlem4  25834  mbfi1flimlem  25838  mbfmullem2  25840  mbfmul  25842  itg20  25853  itg2lea  25860  itg2splitlem  25864  itg2split  25865  itg2monolem1  25866  itg2monolem2  25867  itg2monolem3  25868  itg2mono  25869  itg2i1fseqle  25870  itg2i1fseq  25871  itg2addlem  25874  itg2gt0  25876  itg2cnlem1  25877  itg2cnlem2  25878  itg2cn  25879  itgitg1  25925  bddmulibl  25955  bddibl  25956  dvidlem  26031  dvaddbr  26054  dvmulbr  26055  dvaddf  26058  dvcmulf  26061  dvrec  26071  dvcnvlem  26092  rolle  26106  dveq0  26116  dv11cn  26117  dvivthlem2  26125  dvivth  26126  dvne0  26127  lhop1lem  26129  lhop1  26130  lhop2  26131  lhop  26132  ftc1cn  26159  tdeglem1  26172  tdeglem3  26173  tdeglem4  26174  mdegleb  26178  mdegldg  26180  mdegaddle  26188  ply1remlem  26279  ply1rem  26280  fta1glem1  26282  fta1glem2  26283  fta1blem  26285  idomrootle  26287  plyeq0lem  26324  plyeq0  26325  plyaddlem1  26327  coeeulem  26338  coeaddlem  26363  coemulc  26369  dgradd2  26382  dgrcolem2  26388  ofmulrt  26397  plymul02  26398  plyrem  26423  vieta1lem1  26428  vieta1  26430  plyexmo  26431  elqaalem3  26439  aannenlem1  26446  aalioulem2  26451  ulmuni  26509  ulmdvlem1  26517  ulmdv  26520  mbfulm  26523  iblulm  26524  itgulm  26525  rlimcnp2  27085  jensen  27107  amgm  27109  basellem3  27201  basellem7  27205  basellem9  27207  dchrelbas2  27355  dchrmulcl  27367  dchrfi  27373  dchreq  27376  dchrresb  27377  dchrinv  27379  dchr1re  27381  sumdchr2  27388  dchr2sum  27391  lgsqrlem2  27465  lgsqrlem3  27466  rpvmasum2  27630  dchrisum0re  27631  mirf1o  28896  lmif1o  29043  eqeefv  29158  axlowdimlem14  29210  vtxdgfisf  29731  2pthon3v  30197  nvinvfval  30897  sspg  30985  ssps  30987  sspmlem  30989  sspn  30993  lnon0  31055  ubthlem1  31127  pjfn  31966  kbpj  32213  kbass2  32374  elpjrn  32447  ofrn2  32893  off2  32894  ofresid  32895  xppreima2  32904  ofpreima2  32919  suppovss  32934  resf1o  32983  prodindf  33090  indpreima  33093  swrdrn3  33183  pwrssmgc  33228  mgcf1o  33231  gsumfs2d  33289  gsumhashmul  33295  symgcom2  33312  pmtrcnel  33317  pmtrcnel2  33318  pmtrcnelor  33319  cycpmfvlem  33340  cycpmfv3  33343  cycpmcl  33344  cycpmco2rn  33353  cycpmco2  33361  cycpm3cl2  33364  cyc3co2  33368  cyc3evpm  33378  elrgspnlem1  33470  elrgspnlem2  33471  elrgspnlem4  33473  elrgspnsubrunlem1  33475  elrgspnsubrunlem2  33476  gsumind  33575  islinds5  33592  ellspds  33593  elrspunidl  33647  elrspunsn  33648  rhmimaidl  33651  rprmdvdsprod  33736  1arithidomlem2  33738  evls1fn  33762  ply1dg1rt  33782  ply1mulrtss  33784  ply1degltel  33796  ply1degleel  33797  ply1degltlss  33798  ply1gsumz  33801  ig1pmindeg  33804  r1pquslmic  33812  0mplrim  33816  mplasclco  33818  selvply1rhmlema  33820  selvply1rhmlemb  33821  selvply1rhmlem1  33822  selvply1rhmlem4  33825  selvply1rhm0  33828  extvfvcl  33838  mplmulmvr  33841  evlextv  33844  mplvrpmmhm  33848  mplvrpmrhm  33849  psrmonprod  33854  esplyfval0  33866  esplyfval2  33867  esplyfv1  33871  esplyfv  33872  esplyfval3  33874  esplyfvaln  33876  esplyind  33877  vieta  33882  exsslsb  33899  ply1degltdimlem  33924  ply1degltdim  33925  dimkerim  33929  fedgmullem2  33932  fedgmul  33933  lvecendof1f1o  33935  fldextrspunlsplem  33975  fldextrspunlsp  33976  irngss  33989  irngnzply1  33993  extdgfialglem2  33995  irngnminplynz  34014  2sqr3minply  34082  cos9thpiminply  34090  cmpcref  34152  rhmpreimacnlem  34186  fsumcvg4  34252  pl1cn  34257  qqhval2lem  34283  esumcvg  34388  ofcf  34405  ofcof  34409  measfn  34506  meascnbl  34521  sibfof  34642  sitgaddlemb  34650  subiwrdlen  34688  rrvfn  34747  signsplypnf  34849  signsply0  34850  reprsuc  34914  reprdifc  34926  breprexplema  34929  circlemethhgt  34942  hgt750lemb  34955  f1resrcmplf1dlem  35385  pthhashvtx  35486  cvmopnlem  35636  cvmliftmolem1  35639  cvmliftlem10  35652  cvmlift2lem9a  35661  cvmlift2lem6  35666  cvmlift2lem12  35672  cvmliftphtlem  35675  cvmlift3lem9  35685  mrsubrn  35871  elmrsubrn  35878  elmsubrn  35886  msubrn  35887  mclsind  35928  mclsppslem  35941  mclspps  35942  iprodefisumlem  36098  weiunfrlem  36832  mh-inf3f1  36909  matunitlindflem1  38122  poimirlem1  38127  poimirlem2  38128  poimirlem3  38129  poimirlem16  38142  poimirlem17  38143  poimirlem19  38145  poimirlem20  38146  poimirlem22  38148  poimirlem23  38149  poimirlem29  38155  poimirlem30  38156  poimirlem31  38157  poimir  38159  mblfinlem2  38164  itg2addnclem3  38179  itg2addnc  38180  itg2gt0cn  38181  ftc1cnnc  38198  ftc1anclem5  38203  ftc1anclem7  38205  ftc1anc  38207  sdclem2  38248  istotbnd3  38277  sstotbnd2  38280  isbnd3  38290  heibor1lem  38315  rrnmet  38335  grpokerinj  38399  isdrngo2  38464  lfl1  39701  lfladdcl  39702  lflvscl  39708  lkr0f  39725  lkrsc  39728  eqlkr2  39731  eqlkr3  39732  ldualvaddval  39762  ldualvsval  39769  tendoeq1  41395  zndvdchrrhm  42597  hashscontpow  42746  aks6d1c3  42747  aks6d1c2lem4  42751  aks6d1c2  42754  sticksstones1  42770  sticksstones2  42771  sticksstones3  42772  sticksstones12a  42781  sticksstones12  42782  aks6d1c6lem2  42795  aks6d1c6lem3  42796  aks6d1c6isolem1  42798  aks6d1c6isolem3  42800  aks6d1c6lem5  42801  aks6d1c7lem1  42804  unitscyglem1  42819  dvun  42975  frlmvscadiccat  43135  fiabv  43161  frlmsnic  43165  evlselvlem  43177  evlselv  43178  fsuppssind  43182  mhphf  43186  ismrcd1  43286  ismrcd2  43287  istopclsd  43288  isnacs3  43298  mzpaddmpt  43329  mzpmulmpt  43330  mzpsubst  43336  mzpcong  43556  fnwe2lem2  43635  islmodfg  43653  kercvrlsm  43667  dgrsub2  43719  mpaaeu  43734  rngunsnply  43753  hausgraph  43789  ofoafg  43938  ofoafo  43940  ofoaid1  43942  ofoaid2  43943  naddcnff  43946  naddcnffn  43947  naddcnffo  43948  naddcnfcom  43950  naddcnfid1  43951  naddcnfass  43953  fsovf1od  44599  brcoffn  44613  clsneiel1  44691  wfximgfd  44746  extoimad  44747  mnringmulrcld  44811  mnurndlem1  44850  caofcan  44892  ofmul12  44894  ofdivrec  44895  ofdivcan4  44896  ofdivdiv2  44897  dvconstbi  44903  binomcxplemnotnn0  44925  relpmin  45520  refsum2cnlem1  45616  ssmapsn  45791  preimaiocmnf  46135  fsumsupp0  46153  fsumsermpt  46154  climinf  46181  climinf2lem  46279  limsupmnflem  46293  limsupvaluz2  46311  supcnvlimsup  46313  limsupgtlem  46350  liminfvalxr  46356  liminflelimsupuz  46358  xlimconst2  46408  climxlim2  46419  icccncfext  46460  dvnprodlem1  46519  volicoff  46568  voliooicof  46569  fourierdlem25  46705  fourierdlem48  46727  fourierdlem49  46728  etransclem2  46809  etransclem35  46842  fge0iccico  46943  sge0tsms  46953  sge0sup  46964  sge0resrn  46977  sge0le  46980  sge0fodjrnlem  46989  sge0isum  47000  sge0seq  47019  nnfoctbdjlem  47028  meadjiunlem  47038  omeiunle  47090  hoicvr  47121  ovolval4lem1  47222  ovolval5lem3  47227  ovnovollem1  47229  ovnovollem2  47230  iinhoiicclem  47246  iunhoiioolem  47248  preimaicomnf  47284  smfresal  47361  smfsuplem1  47384  smflimsuplem2  47394  fcoreslem3  47658  fcoreslem4  47659  fcores  47660  isubgredg  48487  upgrimpths  48530  ackvalsucsucval  49320  funchomf  49727  imasubc  49781  imassc  49783  imaid  49784  prcofdiag1  50023  prcofdiag  50024  oppfdiag1  50044  oppfdiag  50046  amgmwlem  50432