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 6556  ⟶wf 6557

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 6565

This theorem is referenced by:  fnconstg  6796  f1fn  6805  fofn  6822  f1ofn  6849  feqmptd  6977  fssrescdmd  7146  fprb  7214  cocan1  7311  oprres  7601  off  7715  coof  7721  ofco  7722  caofref  7728  caofid0l  7730  caofid0r  7731  caofid1  7732  caofid2  7733  caofrss  7736  caoftrn  7738  fo2ndf  8146  fnwelem  8156  fnse  8158  suppsnop  8203  suppss  8219  suppssr  8220  suppssrg  8221  suppssof1  8224  suppofssd  8228  suppofss1d  8229  suppofss2d  8230  suppcoss  8232  smocdmdom  8408  elmapfn  8905  ralxpmap  8936  omxpenlem  9113  mapen  9181  f1finf1o  9305  f1finf1oOLD  9306  unirnffid  9387  fdmfifsupp  9415  mapfien  9448  intrnfi  9456  marypha2  9479  ordtypelem7  9564  wemapsolem  9590  wemapso  9591  wemapso2lem  9592  unxpwdom2  9628  ixpiunwdom  9630  cantnfle  9711  cantnfp1lem2  9719  cantnfp1lem3  9720  cantnfp1  9721  oemapvali  9724  cantnflem1a  9725  cantnflem1c  9727  cantnflem3  9731  cantnf  9733  cnfcomlem  9739  cnfcom3  9744  updjudhcoinlf  9972  updjudhcoinrg  9973  fseqenlem1  10064  numacn  10089  infpwfien  10102  isf32lem2  10394  isf34lem7  10419  isf34lem6  10420  unirnfdomd  10607  ofsubeq0  12263  ofnegsub  12264  ofsubge0  12265  seqf1olem2  14083  resunimafz0  14484  wrdfn  14566  swrdvalfn  14689  pfxfn  14719  pfxid  14722  cats1un  14759  cshwfn  14839  ccatco  14874  limsupgle  15513  o1of2  15649  o1rlimmul  15655  isercolllem2  15702  isercoll  15704  isercoll2  15705  climsup  15706  fsumss  15761  ruclem11  16276  vdwlem2  17020  vdwlem6  17024  vdwlem9  17027  vdwlem12  17030  0ram  17058  ramub1lem1  17064  pwsle  17537  pwsleval  17538  pwsvscaval  17540  mrcuni  17664  mrcun  17665  invf1o  17813  funcres2c  17948  setcmon  18132  setcepi  18133  uncfcurf  18284  yoniso  18330  isacs4lem  18589  acsmapd  18599  gsumval2  18699  mgmhmf1o  18713  resmgmhm2b  18726  mgmhmima  18728  mgmhmeql  18729  prdsplusgsgrpcl  18745  prdssgrpd  18746  prdsplusgcl  18781  prdsidlem  18782  prdsmndd  18783  mhmf1o  18809  resmhm2b  18835  mhmimalem  18837  mhmima  18838  mhmeql  18839  prdspjmhm  18842  pwsco1mhm  18845  pwsco2mhm  18846  gsumwmhm  18858  frmdss2  18876  grpinvf1o  19027  prdsinvlem  19067  cycsubgcl  19224  ghmrn  19247  ghmpreima  19256  ghmeql  19257  ghmnsgima  19258  ghmnsgpreima  19259  ghmeqker  19261  ghmf1o  19266  ghmqusnsglem1  19298  ghmqusnsg  19300  ghmquskerlem1  19301  ghmquskerco  19302  ghmquskerlem3  19304  ghmqusker  19305  gass  19319  cntzmhm  19359  symgextres  19443  gsmsymgrfixlem1  19445  fvcosymgeq  19447  f1omvdconj  19464  pmtrfinv  19479  symgtrinv  19490  pmtr3ncomlem1  19491  sygbasnfpfi  19530  efginvrel2  19745  efgredleme  19761  ghmplusg  19864  prdscmnd  19879  gsumval3a  19921  gsumval3eu  19922  gsumzaddlem  19939  gsumzsplit  19945  gsumpt  19980  prdsgsum  19999  dprdfcntz  20035  dprdfadd  20040  dprdfeq0  20042  dprdf11  20043  dprdlub  20046  dprdspan  20047  dprd2dlem1  20061  dmdprdpr  20069  dprdpr  20070  dpjlem  20071  ablfac1eu  20093  prdsmulrngcl  20172  prdsrngd  20173  prdsringd  20318  prdscrngd  20319  prds1  20320  pwspjmhmmgpd  20325  rnghmf1o  20452  rhmf1o  20491  rhmimasubrnglem  20565  rnrhmsubrg  20605  rrgsupp  20701  imadrhmcl  20798  isabvd  20813  lmodfopnelem1  20896  lcomfsupp  20900  prdsvscacl  20966  prdslmodd  20967  lmhmco  21042  lmhmplusg  21043  lmhmvsca  21044  lmhmf1o  21045  lmhmeql  21054  lspextmo  21055  rhmpreimaidl  21287  pjfo  21735  dsmmbas2  21757  dsmm0cl  21760  dsmmacl  21761  dsmmsubg  21763  dsmmlss  21764  frlmvplusgvalc  21787  frlmvscaval  21788  frlmplusgvalb  21789  frlmvscavalb  21790  frlmsslss2  21795  frlmphllem  21800  frlmphl  21801  frlmssuvc2  21815  frlmsslsp  21816  frlmup1  21818  frlmup2  21819  frlmup3  21820  frlmup4  21821  islindf4  21858  psrbagfsupp  21939  psrbaglesupp  21942  psrbaglecl  21943  psrbagaddcl  21944  psrbagcon  21945  psrbaglefi  21946  psrbagleadd1  21948  psrbagconf1o  21949  gsumbagdiaglem  21950  psrass1lem  21952  psrvscaval  21970  psrlidm  21982  psrridm  21983  psrass1  21984  psrdi  21985  psrdir  21986  psrascl  21999  mvrf2  22013  mplsubglem  22019  mplvscaval  22036  subrgmvrf  22052  mplbas2  22060  mplind  22094  psrbagev1  22101  psrbagev2  22102  evlslem3  22104  evlslem1  22106  evlsvar  22114  mpfind  22131  ismhp3  22146  mhpmulcl  22153  psdmplcl  22166  psdadd  22167  psdvsca  22168  psdmul  22170  psdmvr  22173  psrplusgpropd  22237  coe1add  22267  coe1addfv  22268  evl1addd  22345  evl1subd  22346  evl1muld  22347  pf1mpf  22356  pf1ind  22359  evls1fpws  22373  ressply1evl  22374  rhmply1vsca  22392  mamudir  22408  mamulid  22447  mamurid  22448  mdetrlin  22608  mdetrsca  22609  mdetralt  22614  mdetunilem7  22624  mdetunilem9  22626  madurid  22650  cnrest2  23294  lmss  23306  lmcnp  23312  cnt0  23354  cnt1  23358  cnhaus  23362  rncmp  23404  conncn  23434  2ndcomap  23466  1stccnp  23470  comppfsc  23540  1stckgenlem  23561  ptbasfi  23589  ptopn  23591  ptclsg  23623  ptcnp  23630  upxp  23631  txtube  23648  txcmplem1  23649  hauseqlcld  23654  xkohaus  23661  xkoptsub  23662  cnmpt11  23671  cnmpt21  23679  cnmpt22f  23683  cnmptcom  23686  qtopss  23723  qtopeu  23724  qtopomap  23726  qtopcmap  23727  kqffn  23733  hmeof1o2  23771  xkocnv  23822  rnelfm  23961  ptcmplem1  24060  cnextfres1  24076  ghmcnp  24123  tgphaus  24125  prdstmdd  24132  prdstgpd  24133  fmucnd  24301  psmetxrge0  24323  isxmet2d  24337  prdsmet  24380  blelrnps  24426  blelrn  24427  xmetresbl  24447  comet  24526  stdbdxmet  24528  met2ndci  24535  prdsxmslem2  24542  isngp3  24611  nmotri  24760  metdsre  24875  bndth  24990  evth  24991  fmcfil  25306  bcthlem4  25361  rrxcph  25426  rrxds  25427  rrxmet  25442  evthicc2  25495  ovolfsf  25506  ovolmge0  25512  ovollb2lem  25523  ovolunlem1a  25531  ovoliunlem1  25537  ovoliun  25540  ovoliun2  25541  ovolscalem1  25548  ovolicc1  25551  ovolicc2lem4  25555  ovolicc2  25557  voliunlem1  25585  voliunlem3  25587  volsup  25591  ioombl1lem2  25594  ioombl1lem4  25596  uniiccdif  25613  uniioombllem2  25618  uniioombllem3  25620  uniioombllem6  25623  volsup2  25640  vitalilem4  25646  mbfeqalem1  25676  mbfmulc2lem  25682  mbfmax  25684  mbfaddlem  25695  mbfadd  25696  mbfsub  25697  mbfsup  25699  mbfinf  25700  itg1ge0  25721  itg1addlem1  25727  i1faddlem  25728  i1fmullem  25729  i1fadd  25730  i1fmul  25731  itg1addlem4  25734  i1fmulclem  25737  i1fmulc  25738  itg1mulc  25739  i1fres  25740  itg10a  25745  itg1ge0a  25746  itg1lea  25747  mbfi1fseqlem3  25752  mbfi1fseqlem4  25753  mbfi1flimlem  25757  mbfmullem2  25759  mbfmul  25761  itg20  25772  itg2lea  25779  itg2splitlem  25783  itg2split  25784  itg2monolem1  25785  itg2monolem2  25786  itg2monolem3  25787  itg2mono  25788  itg2i1fseqle  25789  itg2i1fseq  25790  itg2addlem  25793  itg2gt0  25795  itg2cnlem1  25796  itg2cnlem2  25797  itg2cn  25798  itgitg1  25844  bddmulibl  25874  bddibl  25875  dvidlem  25950  dvaddbr  25974  dvmulbr  25975  dvmulbrOLD  25976  dvaddf  25979  dvcmulf  25982  dvrec  25993  dvcnvlem  26014  rolle  26028  dveq0  26039  dv11cn  26040  dvivthlem2  26048  dvivth  26049  dvne0  26050  lhop1lem  26052  lhop1  26053  lhop2  26054  lhop  26055  ftc1cn  26084  tdeglem1  26097  tdeglem3  26098  tdeglem4  26099  mdegleb  26103  mdegldg  26105  mdegaddle  26113  ply1remlem  26204  ply1rem  26205  fta1glem1  26207  fta1glem2  26208  fta1blem  26210  idomrootle  26212  plyeq0lem  26249  plyeq0  26250  plyaddlem1  26252  coeeulem  26263  coeaddlem  26288  coemulc  26294  dgradd2  26308  dgrcolem2  26314  ofmulrt  26323  plyrem  26347  vieta1lem1  26352  vieta1  26354  plyexmo  26355  elqaalem3  26363  aannenlem1  26370  aalioulem2  26375  ulmuni  26435  ulmdvlem1  26443  ulmdv  26446  mbfulm  26449  iblulm  26450  itgulm  26451  rlimcnp2  27009  jensen  27032  amgm  27034  basellem3  27126  basellem7  27130  basellem9  27132  dchrelbas2  27281  dchrmulcl  27293  dchrfi  27299  dchreq  27302  dchrresb  27303  dchrinv  27305  dchr1re  27307  sumdchr2  27314  dchr2sum  27317  lgsqrlem2  27391  lgsqrlem3  27392  rpvmasum2  27556  dchrisum0re  27557  mirf1o  28677  lmif1o  28803  eqeefv  28918  axlowdimlem14  28970  vtxdgfisf  29494  2pthon3v  29963  nvinvfval  30659  sspg  30747  ssps  30749  sspmlem  30751  sspn  30755  lnon0  30817  ubthlem1  30889  pjfn  31728  kbpj  31975  kbass2  32136  elpjrn  32209  ofrn2  32650  off2  32651  ofresid  32652  xppreima2  32661  ofpreima2  32676  suppovss  32690  resf1o  32741  prodindf  32848  indpreima  32850  swrdrn3  32940  pwrssmgc  32990  mgcf1o  32993  chnso  33004  gsumfs2d  33058  gsumhashmul  33064  gsumle  33101  symgcom2  33104  pmtrcnel  33109  pmtrcnel2  33110  pmtrcnelor  33111  cycpmfvlem  33132  cycpmfv3  33135  cycpmcl  33136  cycpmco2rn  33145  cycpmco2  33153  cycpm3cl2  33156  cyc3co2  33160  cyc3evpm  33170  elrgspnlem1  33246  elrgspnlem2  33247  elrgspnlem4  33249  elrgspnsubrunlem1  33251  elrgspnsubrunlem2  33252  islinds5  33395  ellspds  33396  elrspunidl  33456  elrspunsn  33457  rhmimaidl  33460  rhmpreimaprmidl  33479  rprmdvdsprod  33562  1arithidomlem2  33564  evls1fn  33586  ply1dg1rt  33604  ply1mulrtss  33606  ply1degltel  33615  ply1degleel  33616  ply1degltlss  33617  ply1gsumz  33619  ig1pmindeg  33622  r1pquslmic  33631  exsslsb  33647  ply1degltdimlem  33673  ply1degltdim  33674  dimkerim  33678  fedgmullem2  33681  fedgmul  33682  lvecendof1f1o  33684  fldextrspunlsplem  33723  fldextrspunlsp  33724  irngss  33737  irngnzply1  33741  irngnminplynz  33755  2sqr3minply  33791  cmpcref  33849  rhmpreimacnlem  33883  fsumcvg4  33949  pl1cn  33954  qqhval2lem  33982  esumcvg  34087  ofcf  34104  ofcof  34108  measfn  34205  meascnbl  34220  sibfof  34342  sitgaddlemb  34350  subiwrdlen  34388  rrvfn  34447  plymul02  34561  signsplypnf  34565  signsply0  34566  reprsuc  34630  reprdifc  34642  breprexplema  34645  circlemethhgt  34658  hgt750lemb  34671  f1resrcmplf1dlem  35100  pthhashvtx  35133  cvmopnlem  35283  cvmliftmolem1  35286  cvmliftlem10  35299  cvmlift2lem9a  35308  cvmlift2lem6  35313  cvmlift2lem12  35319  cvmliftphtlem  35322  cvmlift3lem9  35332  mrsubrn  35518  elmrsubrn  35525  elmsubrn  35533  msubrn  35534  mclsind  35575  mclsppslem  35588  mclspps  35589  iprodefisumlem  35740  weiunfrlem  36465  matunitlindflem1  37623  poimirlem1  37628  poimirlem2  37629  poimirlem3  37630  poimirlem16  37643  poimirlem17  37644  poimirlem19  37646  poimirlem20  37647  poimirlem22  37649  poimirlem23  37650  poimirlem29  37656  poimirlem30  37657  poimirlem31  37658  poimir  37660  mblfinlem2  37665  itg2addnclem3  37680  itg2addnc  37681  itg2gt0cn  37682  ftc1cnnc  37699  ftc1anclem5  37704  ftc1anclem7  37706  ftc1anc  37708  sdclem2  37749  istotbnd3  37778  sstotbnd2  37781  isbnd3  37791  heibor1lem  37816  rrnmet  37836  grpokerinj  37900  isdrngo2  37965  lfl1  39071  lfladdcl  39072  lflvscl  39078  lkr0f  39095  lkrsc  39098  eqlkr2  39101  eqlkr3  39102  ldualvaddval  39132  ldualvsval  39139  tendoeq1  40766  zndvdchrrhm  41972  hashscontpow  42123  aks6d1c3  42124  aks6d1c2lem4  42128  aks6d1c2  42131  sticksstones1  42147  sticksstones2  42148  sticksstones3  42149  sticksstones12a  42158  sticksstones12  42159  aks6d1c6lem2  42172  aks6d1c6lem3  42173  aks6d1c6isolem1  42175  aks6d1c6isolem3  42177  aks6d1c6lem5  42178  aks6d1c7lem1  42181  unitscyglem1  42196  metakunt19  42224  metakunt25  42230  metakunt33  42238  dvun  42389  frlmvscadiccat  42516  fiabv  42546  frlmsnic  42550  pwsgprod  42554  mplmapghm  42566  evlsvvval  42573  evlsaddval  42578  evlsmulval  42579  evladdval  42585  evlmulval  42586  selvvvval  42595  evlselvlem  42596  evlselv  42597  fsuppssind  42603  mhphf  42607  ismrcd1  42709  ismrcd2  42710  istopclsd  42711  isnacs3  42721  mzpaddmpt  42752  mzpmulmpt  42753  mzpsubst  42759  mzpcong  42984  fnwe2lem2  43063  islmodfg  43081  kercvrlsm  43095  dgrsub2  43147  mpaaeu  43162  rngunsnply  43181  hausgraph  43217  ofoafg  43367  ofoafo  43369  ofoaid1  43371  ofoaid2  43372  naddcnff  43375  naddcnffn  43376  naddcnffo  43377  naddcnfcom  43379  naddcnfid1  43380  naddcnfass  43382  fsovf1od  44029  brcoffn  44043  clsneiel1  44121  wfximgfd  44176  extoimad  44177  mnringmulrcld  44247  mnurndlem1  44300  caofcan  44342  ofmul12  44344  ofdivrec  44345  ofdivcan4  44346  ofdivdiv2  44347  dvconstbi  44353  binomcxplemnotnn0  44375  relpmin  44973  refsum2cnlem1  45042  ssmapsn  45221  preimaiocmnf  45574  fsumsupp0  45593  fsumsermpt  45594  climinf  45621  climinf2lem  45721  limsupmnflem  45735  limsupvaluz2  45753  supcnvlimsup  45755  limsupgtlem  45792  liminfvalxr  45798  liminflelimsupuz  45800  xlimconst2  45850  climxlim2  45861  icccncfext  45902  dvnprodlem1  45961  volicoff  46010  voliooicof  46011  fourierdlem25  46147  etransclem2  46251  etransclem35  46284  fge0iccico  46385  sge0tsms  46395  sge0sup  46406  sge0resrn  46419  sge0le  46422  sge0fodjrnlem  46431  sge0isum  46442  sge0seq  46461  nnfoctbdjlem  46470  meadjiunlem  46480  omeiunle  46532  hoicvr  46563  ovolval4lem1  46664  ovolval5lem3  46669  ovnovollem1  46671  ovnovollem2  46672  iinhoiicclem  46688  iunhoiioolem  46690  preimaicomnf  46726  smfresal  46803  smfsuplem1  46826  smflimsuplem2  46836  fcoreslem3  47077  fcoreslem4  47078  fcores  47079  isubgredg  47852  ackvalsucsucval  48609  amgmwlem  49321