Theorem ffnd 6748

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

Syntax hints:   → wi 4   Fn wfn 6568  ⟶wf 6569

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 6577

This theorem is referenced by:  fnconstg  6809  f1fn  6818  fofn  6836  f1ofn  6863  feqmptd  6990  fssrescdmd  7160  fprb  7231  cocan1  7327  oprres  7618  off  7732  coof  7737  ofco  7738  caofref  7744  caofid0l  7746  caofid0r  7747  caofid1  7748  caofid2  7749  caofrss  7751  caoftrn  7753  fo2ndf  8162  fnwelem  8172  fnse  8174  suppsnop  8219  suppss  8235  suppssr  8236  suppssrg  8237  suppssof1  8240  suppofssd  8244  suppofss1d  8245  suppofss2d  8246  suppcoss  8248  smocdmdom  8424  elmapfn  8923  ralxpmap  8954  omxpenlem  9139  mapen  9207  f1finf1o  9333  f1finf1oOLD  9334  unirnffid  9415  fdmfifsupp  9444  mapfien  9477  intrnfi  9485  marypha2  9508  ordtypelem7  9593  wemapsolem  9619  wemapso  9620  wemapso2lem  9621  unxpwdom2  9657  ixpiunwdom  9659  cantnfle  9740  cantnfp1lem2  9748  cantnfp1lem3  9749  cantnfp1  9750  oemapvali  9753  cantnflem1a  9754  cantnflem1c  9756  cantnflem3  9760  cantnf  9762  cnfcomlem  9768  cnfcom3  9773  updjudhcoinlf  10001  updjudhcoinrg  10002  fseqenlem1  10093  numacn  10118  infpwfien  10131  isf32lem2  10423  isf34lem7  10448  isf34lem6  10449  unirnfdomd  10636  ofsubeq0  12290  ofnegsub  12291  ofsubge0  12292  seqf1olem2  14093  resunimafz0  14494  wrdfn  14576  swrdvalfn  14699  pfxfn  14729  pfxid  14732  cats1un  14769  cshwfn  14849  ccatco  14884  limsupgle  15523  o1of2  15659  o1rlimmul  15665  isercolllem2  15714  isercoll  15716  isercoll2  15717  climsup  15718  fsumss  15773  ruclem11  16288  vdwlem2  17029  vdwlem6  17033  vdwlem9  17036  vdwlem12  17039  0ram  17067  ramub1lem1  17073  pwsle  17552  pwsleval  17553  pwsvscaval  17555  mrcuni  17679  mrcun  17680  invf1o  17830  funcres2c  17968  setcmon  18154  setcepi  18155  uncfcurf  18309  yoniso  18355  isacs4lem  18614  acsmapd  18624  gsumval2  18724  mgmhmf1o  18738  resmgmhm2b  18751  mgmhmima  18753  mgmhmeql  18754  prdsplusgsgrpcl  18770  prdssgrpd  18771  prdsplusgcl  18803  prdsidlem  18804  prdsmndd  18805  mhmf1o  18831  resmhm2b  18857  mhmimalem  18859  mhmima  18860  mhmeql  18861  prdspjmhm  18864  pwsco1mhm  18867  pwsco2mhm  18868  gsumwmhm  18880  frmdss2  18898  grpinvf1o  19049  prdsinvlem  19089  cycsubgcl  19246  ghmrn  19269  ghmpreima  19278  ghmeql  19279  ghmnsgima  19280  ghmnsgpreima  19281  ghmeqker  19283  ghmf1o  19288  ghmqusnsglem1  19320  ghmqusnsg  19322  ghmquskerlem1  19323  ghmquskerco  19324  ghmquskerlem3  19326  ghmqusker  19327  gass  19341  cntzmhm  19381  symgextres  19467  gsmsymgrfixlem1  19469  fvcosymgeq  19471  f1omvdconj  19488  pmtrfinv  19503  symgtrinv  19514  pmtr3ncomlem1  19515  sygbasnfpfi  19554  efginvrel2  19769  efgredleme  19785  ghmplusg  19888  prdscmnd  19903  gsumval3a  19945  gsumval3eu  19946  gsumzaddlem  19963  gsumzsplit  19969  gsumpt  20004  prdsgsum  20023  dprdfcntz  20059  dprdfadd  20064  dprdfeq0  20066  dprdf11  20067  dprdlub  20070  dprdspan  20071  dprd2dlem1  20085  dmdprdpr  20093  dprdpr  20094  dpjlem  20095  ablfac1eu  20117  prdsmulrngcl  20202  prdsrngd  20203  prdsringd  20344  prdscrngd  20345  prds1  20346  pwspjmhmmgpd  20351  rnghmf1o  20478  rhmf1o  20517  rhmimasubrnglem  20591  rnrhmsubrg  20633  rrgsupp  20723  imadrhmcl  20820  isabvd  20835  lmodfopnelem1  20918  lcomfsupp  20922  prdsvscacl  20989  prdslmodd  20990  lmhmco  21065  lmhmplusg  21066  lmhmvsca  21067  lmhmf1o  21068  lmhmeql  21077  lspextmo  21078  rhmpreimaidl  21310  pjfo  21758  dsmmbas2  21780  dsmm0cl  21783  dsmmacl  21784  dsmmsubg  21786  dsmmlss  21787  frlmvplusgvalc  21810  frlmvscaval  21811  frlmplusgvalb  21812  frlmvscavalb  21813  frlmsslss2  21818  frlmphllem  21823  frlmphl  21824  frlmssuvc2  21838  frlmsslsp  21839  frlmup1  21841  frlmup2  21842  frlmup3  21843  frlmup4  21844  islindf4  21881  psrbagfsupp  21962  psrbaglesupp  21965  psrbaglecl  21966  psrbagaddcl  21967  psrbagcon  21968  psrbaglefi  21969  psrbagleadd1  21971  psrbagconf1o  21972  gsumbagdiaglem  21973  psrass1lem  21975  psrvscaval  21993  psrlidm  22005  psrridm  22006  psrass1  22007  psrdi  22008  psrdir  22009  psrascl  22022  mvrf2  22036  mplsubglem  22042  mplvscaval  22059  subrgmvrf  22075  mplbas2  22083  mplind  22117  psrbagev1  22124  psrbagev2  22125  evlslem3  22127  evlslem1  22129  evlsvar  22137  mpfind  22154  ismhp3  22169  mhpmulcl  22176  psdmplcl  22189  psdadd  22190  psdvsca  22191  psdmul  22193  psrplusgpropd  22258  coe1add  22288  coe1addfv  22289  evl1addd  22366  evl1subd  22367  evl1muld  22368  pf1mpf  22377  pf1ind  22380  evls1fpws  22394  ressply1evl  22395  rhmply1vsca  22413  mamudir  22429  mamulid  22468  mamurid  22469  mdetrlin  22629  mdetrsca  22630  mdetralt  22635  mdetunilem7  22645  mdetunilem9  22647  madurid  22671  cnrest2  23315  lmss  23327  lmcnp  23333  cnt0  23375  cnt1  23379  cnhaus  23383  rncmp  23425  conncn  23455  2ndcomap  23487  1stccnp  23491  comppfsc  23561  1stckgenlem  23582  ptbasfi  23610  ptopn  23612  ptclsg  23644  ptcnp  23651  upxp  23652  txtube  23669  txcmplem1  23670  hauseqlcld  23675  xkohaus  23682  xkoptsub  23683  cnmpt11  23692  cnmpt21  23700  cnmpt22f  23704  cnmptcom  23707  qtopss  23744  qtopeu  23745  qtopomap  23747  qtopcmap  23748  kqffn  23754  hmeof1o2  23792  xkocnv  23843  rnelfm  23982  ptcmplem1  24081  cnextfres1  24097  ghmcnp  24144  tgphaus  24146  prdstmdd  24153  prdstgpd  24154  fmucnd  24322  psmetxrge0  24344  isxmet2d  24358  prdsmet  24401  blelrnps  24447  blelrn  24448  xmetresbl  24468  comet  24547  stdbdxmet  24549  met2ndci  24556  prdsxmslem2  24563  isngp3  24632  nmotri  24781  metdsre  24894  bndth  25009  evth  25010  fmcfil  25325  bcthlem4  25380  rrxcph  25445  rrxds  25446  rrxmet  25461  evthicc2  25514  ovolfsf  25525  ovolmge0  25531  ovollb2lem  25542  ovolunlem1a  25550  ovoliunlem1  25556  ovoliun  25559  ovoliun2  25560  ovolscalem1  25567  ovolicc1  25570  ovolicc2lem4  25574  ovolicc2  25576  voliunlem1  25604  voliunlem3  25606  volsup  25610  ioombl1lem2  25613  ioombl1lem4  25615  uniiccdif  25632  uniioombllem2  25637  uniioombllem3  25639  uniioombllem6  25642  volsup2  25659  vitalilem4  25665  mbfeqalem1  25695  mbfmulc2lem  25701  mbfmax  25703  mbfaddlem  25714  mbfadd  25715  mbfsub  25716  mbfsup  25718  mbfinf  25719  itg1ge0  25740  itg1addlem1  25746  i1faddlem  25747  i1fmullem  25748  i1fadd  25749  i1fmul  25750  itg1addlem4  25753  itg1addlem4OLD  25754  i1fmulclem  25757  i1fmulc  25758  itg1mulc  25759  i1fres  25760  itg10a  25765  itg1ge0a  25766  itg1lea  25767  mbfi1fseqlem3  25772  mbfi1fseqlem4  25773  mbfi1flimlem  25777  mbfmullem2  25779  mbfmul  25781  itg20  25792  itg2lea  25799  itg2splitlem  25803  itg2split  25804  itg2monolem1  25805  itg2monolem2  25806  itg2monolem3  25807  itg2mono  25808  itg2i1fseqle  25809  itg2i1fseq  25810  itg2addlem  25813  itg2gt0  25815  itg2cnlem1  25816  itg2cnlem2  25817  itg2cn  25818  itgitg1  25864  bddmulibl  25894  bddibl  25895  dvidlem  25970  dvaddbr  25994  dvmulbr  25995  dvmulbrOLD  25996  dvaddf  25999  dvcmulf  26002  dvrec  26013  dvcnvlem  26034  rolle  26048  dveq0  26059  dv11cn  26060  dvivthlem2  26068  dvivth  26069  dvne0  26070  lhop1lem  26072  lhop1  26073  lhop2  26074  lhop  26075  ftc1cn  26104  tdeglem1  26117  tdeglem3  26118  tdeglem4  26119  mdegleb  26123  mdegldg  26125  mdegaddle  26133  ply1remlem  26224  ply1rem  26225  fta1glem1  26227  fta1glem2  26228  fta1blem  26230  idomrootle  26232  plyeq0lem  26269  plyeq0  26270  plyaddlem1  26272  coeeulem  26283  coeaddlem  26308  coemulc  26314  dgradd2  26328  dgrcolem2  26334  ofmulrt  26341  plyrem  26365  vieta1lem1  26370  vieta1  26372  plyexmo  26373  elqaalem3  26381  aannenlem1  26388  aalioulem2  26393  ulmuni  26453  ulmdvlem1  26461  ulmdv  26464  mbfulm  26467  iblulm  26468  itgulm  26469  rlimcnp2  27027  jensen  27050  amgm  27052  basellem3  27144  basellem7  27148  basellem9  27150  dchrelbas2  27299  dchrmulcl  27311  dchrfi  27317  dchreq  27320  dchrresb  27321  dchrinv  27323  dchr1re  27325  sumdchr2  27332  dchr2sum  27335  lgsqrlem2  27409  lgsqrlem3  27410  rpvmasum2  27574  dchrisum0re  27575  mirf1o  28695  lmif1o  28821  eqeefv  28936  axlowdimlem14  28988  vtxdgfisf  29512  2pthon3v  29976  nvinvfval  30672  sspg  30760  ssps  30762  sspmlem  30764  sspn  30768  lnon0  30830  ubthlem1  30902  pjfn  31741  kbpj  31988  kbass2  32149  elpjrn  32222  ofrn2  32659  off2  32660  ofresid  32661  xppreima2  32669  ofpreima2  32684  suppovss  32697  resf1o  32744  swrdrn3  32922  pwrssmgc  32973  mgcf1o  32976  chnso  32986  gsumhashmul  33040  gsumle  33074  symgcom2  33077  pmtrcnel  33082  pmtrcnel2  33083  pmtrcnelor  33084  cycpmfvlem  33105  cycpmfv3  33108  cycpmcl  33109  cycpmco2rn  33118  cycpmco2  33126  cycpm3cl2  33129  cyc3co2  33133  cyc3evpm  33143  islinds5  33360  ellspds  33361  elrspunidl  33421  elrspunsn  33422  rhmimaidl  33425  rhmpreimaprmidl  33444  rprmdvdsprod  33527  1arithidomlem2  33529  evls1fn  33551  ply1dg1rt  33569  ply1mulrtss  33571  ply1degltel  33580  ply1degleel  33581  ply1degltlss  33582  ply1gsumz  33584  ig1pmindeg  33587  r1pquslmic  33596  ply1degltdimlem  33635  ply1degltdim  33636  dimkerim  33640  fedgmullem2  33643  fedgmul  33644  lvecendof1f1o  33646  irngss  33687  irngnzply1  33691  irngnminplynz  33705  2sqr3minply  33738  cmpcref  33796  rhmpreimacnlem  33830  fsumcvg4  33896  pl1cn  33901  qqhval2lem  33927  prodindf  33987  indpreima  33989  esumcvg  34050  ofcf  34067  ofcof  34071  measfn  34168  meascnbl  34183  sibfof  34305  sitgaddlemb  34313  subiwrdlen  34351  rrvfn  34410  plymul02  34523  signsplypnf  34527  signsply0  34528  reprsuc  34592  reprdifc  34604  breprexplema  34607  circlemethhgt  34620  hgt750lemb  34633  f1resrcmplf1dlem  35062  pthhashvtx  35095  cvmopnlem  35246  cvmliftmolem1  35249  cvmliftlem10  35262  cvmlift2lem9a  35271  cvmlift2lem6  35276  cvmlift2lem12  35282  cvmliftphtlem  35285  cvmlift3lem9  35295  mrsubrn  35481  elmrsubrn  35488  elmsubrn  35496  msubrn  35497  mclsind  35538  mclsppslem  35551  mclspps  35552  iprodefisumlem  35702  weiunfrlem  36430  matunitlindflem1  37576  poimirlem1  37581  poimirlem2  37582  poimirlem3  37583  poimirlem16  37596  poimirlem17  37597  poimirlem19  37599  poimirlem20  37600  poimirlem22  37602  poimirlem23  37603  poimirlem29  37609  poimirlem30  37610  poimirlem31  37611  poimir  37613  mblfinlem2  37618  itg2addnclem3  37633  itg2addnc  37634  itg2gt0cn  37635  ftc1cnnc  37652  ftc1anclem5  37657  ftc1anclem7  37659  ftc1anc  37661  sdclem2  37702  istotbnd3  37731  sstotbnd2  37734  isbnd3  37744  heibor1lem  37769  rrnmet  37789  grpokerinj  37853  isdrngo2  37918  lfl1  39026  lfladdcl  39027  lflvscl  39033  lkr0f  39050  lkrsc  39053  eqlkr2  39056  eqlkr3  39057  ldualvaddval  39087  ldualvsval  39094  tendoeq1  40721  zndvdchrrhm  41927  hashscontpow  42079  aks6d1c3  42080  aks6d1c2lem4  42084  aks6d1c2  42087  sticksstones1  42103  sticksstones2  42104  sticksstones3  42105  sticksstones12a  42114  sticksstones12  42115  aks6d1c6lem2  42128  aks6d1c6lem3  42129  aks6d1c6isolem1  42131  aks6d1c6isolem3  42133  aks6d1c6lem5  42134  aks6d1c7lem1  42137  unitscyglem1  42152  metakunt19  42180  metakunt25  42186  metakunt33  42194  frlmvscadiccat  42461  fiabv  42491  frlmsnic  42495  pwsgprod  42499  mplmapghm  42511  evlsvvval  42518  evlsaddval  42523  evlsmulval  42524  evladdval  42530  evlmulval  42531  selvvvval  42540  evlselvlem  42541  evlselv  42542  fsuppssind  42548  mhphf  42552  ismrcd1  42654  ismrcd2  42655  istopclsd  42656  isnacs3  42666  mzpaddmpt  42697  mzpmulmpt  42698  mzpsubst  42704  mzpcong  42929  fnwe2lem2  43008  islmodfg  43026  kercvrlsm  43040  dgrsub2  43092  mpaaeu  43107  rngunsnply  43130  hausgraph  43166  ofoafg  43316  ofoafo  43318  ofoaid1  43320  ofoaid2  43321  naddcnff  43324  naddcnffn  43325  naddcnffo  43326  naddcnfcom  43328  naddcnfid1  43329  naddcnfass  43331  fsovf1od  43978  brcoffn  43992  clsneiel1  44070  wfximgfd  44125  extoimad  44126  mnringmulrcld  44197  mnurndlem1  44250  caofcan  44292  ofmul12  44294  ofdivrec  44295  ofdivcan4  44296  ofdivdiv2  44297  dvconstbi  44303  binomcxplemnotnn0  44325  refsum2cnlem1  44937  ssmapsn  45123  preimaiocmnf  45479  fsumsupp0  45499  fsumsermpt  45500  climinf  45527  climinf2lem  45627  limsupmnflem  45641  limsupvaluz2  45659  supcnvlimsup  45661  limsupgtlem  45698  liminfvalxr  45704  liminflelimsupuz  45706  xlimconst2  45756  climxlim2  45767  icccncfext  45808  dvnprodlem1  45867  volicoff  45916  voliooicof  45917  fourierdlem25  46053  etransclem2  46157  etransclem35  46190  fge0iccico  46291  sge0tsms  46301  sge0sup  46312  sge0resrn  46325  sge0le  46328  sge0fodjrnlem  46337  sge0isum  46348  sge0seq  46367  nnfoctbdjlem  46376  meadjiunlem  46386  omeiunle  46438  hoicvr  46469  ovolval4lem1  46570  ovolval5lem3  46575  ovnovollem1  46577  ovnovollem2  46578  iinhoiicclem  46594  iunhoiioolem  46596  preimaicomnf  46632  smfresal  46709  smfsuplem1  46732  smflimsuplem2  46742  fcoreslem3  46980  fcoreslem4  46981  fcores  46982  ackvalsucsucval  48422  amgmwlem  48896