Theorem ffnd 6514

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

Syntax hints:   → wi 4   Fn wfn 6349  ⟶wf 6350

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 209  df-an 399  df-f 6358

This theorem is referenced by:  fnconstg  6566  f1fn  6575  fofn  6591  f1ofn  6615  feqmptd  6732  fprb  6955  rnmptcOLD  6969  cocan1  7046  oprres  7315  off  7423  ofco  7428  caofref  7434  caofid0l  7436  caofid0r  7437  caofid1  7438  caofid2  7439  caofrss  7441  caoftrn  7443  fo2ndf  7816  fnwelem  7824  fnse  7826  suppsnop  7843  suppss  7859  suppssr  7860  suppssof1  7862  suppofssd  7866  suppofss1d  7867  suppofss2d  7868  smorndom  8004  elmapfn  8428  ralxpmap  8459  omxpenlem  8617  mapen  8680  f1finf1o  8744  unirnffid  8815  fdmfifsupp  8842  mapfien  8870  intrnfi  8879  marypha2  8902  ordtypelem7  8987  wemapsolem  9013  wemapso  9014  wemapso2lem  9015  unxpwdom2  9051  ixpiunwdom  9054  cantnfle  9133  cantnfp1lem2  9141  cantnfp1lem3  9142  cantnfp1  9143  oemapvali  9146  cantnflem1a  9147  cantnflem1c  9149  cantnflem3  9153  cantnf  9155  cnfcomlem  9161  cnfcom3  9166  updjudhcoinlf  9360  updjudhcoinrg  9361  fseqenlem1  9449  numacn  9474  infpwfien  9487  isf32lem2  9775  isf34lem7  9800  isf34lem6  9801  unirnfdomd  9988  ofsubeq0  11634  ofnegsub  11635  ofsubge0  11636  seqf1olem2  13409  resunimafz0  13802  wrdfn  13875  swrdvalfn  14012  pfxfn  14042  pfxid  14045  cats1un  14082  cshwfn  14162  ccatco  14196  limsupgle  14833  o1of2  14968  o1rlimmul  14974  isercolllem2  15021  isercoll  15023  isercoll2  15024  climsup  15025  fsumss  15081  ruclem11  15592  vdwlem2  16317  vdwlem6  16321  vdwlem9  16324  vdwlem12  16327  0ram  16355  ramub1lem1  16361  pwsle  16764  pwsleval  16765  pwsvscaval  16767  mrcuni  16891  mrcun  16892  invf1o  17038  funcres2c  17170  setcmon  17346  setcepi  17347  uncfcurf  17488  yoniso  17534  isacs4lem  17777  acsmapd  17787  gsumval2  17895  prdsplusgcl  17941  prdsidlem  17942  prdsmndd  17943  mhmf1o  17965  resmhm2b  17986  mhmima  17988  mhmeql  17989  prdspjmhm  17992  pwsco1mhm  17995  pwsco2mhm  17996  gsumwmhm  18009  frmdss2  18027  grpinvf1o  18168  prdsinvlem  18207  cycsubgcl  18348  ghmrn  18370  ghmpreima  18379  ghmeql  18380  ghmnsgima  18381  ghmnsgpreima  18382  ghmeqker  18384  ghmf1o  18387  gass  18430  cntzmhm  18468  symgextres  18552  gsmsymgrfixlem1  18554  fvcosymgeq  18556  f1omvdconj  18573  pmtrfinv  18588  symgtrinv  18599  pmtr3ncomlem1  18600  sygbasnfpfi  18639  efginvrel2  18852  efgredleme  18868  ghmplusg  18965  prdscmnd  18980  gsumval3a  19022  gsumval3eu  19023  gsumzaddlem  19040  gsumzsplit  19046  gsumpt  19081  prdsgsum  19100  dprdfcntz  19136  dprdfadd  19141  dprdfeq0  19143  dprdf11  19144  dprdlub  19147  dprdspan  19148  dprd2dlem1  19162  dmdprdpr  19170  dprdpr  19171  dpjlem  19172  ablfac1eu  19194  prdsmulrcl  19360  prdsringd  19361  prdscrngd  19362  prds1  19363  rhmf1o  19483  rnrhmsubrg  19566  isabvd  19590  lmodfopnelem1  19669  lcomfsupp  19673  prdsvscacl  19739  prdslmodd  19740  lmhmco  19814  lmhmplusg  19815  lmhmvsca  19816  lmhmf1o  19817  lmhmeql  19826  lspextmo  19827  rrgsupp  20063  psrbaglesupp  20147  psrbagcon  20150  psrbaglefi  20151  psrbagconf1o  20153  gsumbagdiaglem  20154  psrvscaval  20171  psrlidm  20182  psrridm  20183  psrass1  20184  psrdi  20185  psrdir  20186  mplsubglem  20213  mplvscaval  20227  subrgmvrf  20242  mplbas2  20250  mvrf2  20271  mplind  20281  psrbagev1  20289  evlslem3  20292  evlslem1  20294  evlsvar  20302  mpfind  20319  mhpinvcl  20338  psrplusgpropd  20403  coe1add  20431  coe1addfv  20432  evl1addd  20503  evl1subd  20504  evl1muld  20505  pf1mpf  20514  pf1ind  20517  pjfo  20858  dsmmbas2  20880  dsmm0cl  20883  dsmmacl  20884  dsmmsubg  20886  dsmmlss  20887  frlmvplusgvalc  20910  frlmvscaval  20911  frlmplusgvalb  20912  frlmvscavalb  20913  frlmsslss2  20918  frlmphllem  20923  frlmphl  20924  frlmssuvc2  20938  frlmsslsp  20939  frlmup1  20941  frlmup2  20942  frlmup3  20943  frlmup4  20944  islindf4  20981  mamudir  21012  mamulid  21049  mamurid  21050  mdetrlin  21210  mdetrsca  21211  mdetralt  21216  mdetunilem7  21226  mdetunilem9  21228  madurid  21252  cnrest2  21893  lmss  21905  lmcnp  21911  cnt0  21953  cnt1  21957  cnhaus  21961  rncmp  22003  conncn  22033  2ndcomap  22065  1stccnp  22069  comppfsc  22139  1stckgenlem  22160  ptbasfi  22188  ptopn  22190  ptclsg  22222  ptcnp  22229  upxp  22230  txtube  22247  txcmplem1  22248  hauseqlcld  22253  xkohaus  22260  xkoptsub  22261  cnmpt11  22270  cnmpt21  22278  cnmpt22f  22282  cnmptcom  22285  qtopss  22322  qtopeu  22323  qtopomap  22325  qtopcmap  22326  kqffn  22332  hmeof1o2  22370  xkocnv  22421  rnelfm  22560  ptcmplem1  22659  cnextfres1  22675  ghmcnp  22722  tgphaus  22724  prdstmdd  22731  prdstgpd  22732  fmucnd  22900  psmetxrge0  22922  isxmet2d  22936  prdsmet  22979  blelrnps  23025  blelrn  23026  xmetresbl  23046  comet  23122  stdbdxmet  23124  met2ndci  23131  prdsxmslem2  23138  isngp3  23206  nmotri  23347  metdsre  23460  bndth  23561  evth  23562  fmcfil  23874  bcthlem4  23929  rrxcph  23994  rrxds  23995  rrxmet  24010  evthicc2  24060  ovolfsf  24071  ovolmge0  24077  ovollb2lem  24088  ovolunlem1a  24096  ovoliunlem1  24102  ovoliun  24105  ovoliun2  24106  ovolscalem1  24113  ovolicc1  24116  ovolicc2lem4  24120  ovolicc2  24122  voliunlem1  24150  voliunlem3  24152  volsup  24156  ioombl1lem2  24159  ioombl1lem4  24161  uniiccdif  24178  uniioombllem2  24183  uniioombllem3  24185  uniioombllem6  24188  volsup2  24205  vitalilem4  24211  mbfeqalem1  24241  mbfmulc2lem  24247  mbfmax  24249  mbfaddlem  24260  mbfadd  24261  mbfsub  24262  mbfsup  24264  mbfinf  24265  itg1ge0  24286  itg1addlem1  24292  i1faddlem  24293  i1fmullem  24294  i1fadd  24295  i1fmul  24296  itg1addlem4  24299  i1fmulclem  24302  i1fmulc  24303  itg1mulc  24304  i1fres  24305  itg10a  24310  itg1ge0a  24311  itg1lea  24312  mbfi1fseqlem3  24317  mbfi1fseqlem4  24318  mbfi1flimlem  24322  mbfmullem2  24324  mbfmul  24326  itg20  24337  itg2lea  24344  itg2splitlem  24348  itg2split  24349  itg2monolem1  24350  itg2monolem2  24351  itg2monolem3  24352  itg2mono  24353  itg2i1fseqle  24354  itg2i1fseq  24355  itg2addlem  24358  itg2gt0  24360  itg2cnlem1  24361  itg2cnlem2  24362  itg2cn  24363  itgitg1  24408  bddmulibl  24438  bddibl  24439  dvidlem  24512  dvaddbr  24534  dvmulbr  24535  dvaddf  24538  dvcmulf  24541  dvrec  24551  dvcnvlem  24572  rolle  24586  dveq0  24596  dv11cn  24597  dvivthlem2  24605  dvivth  24606  dvne0  24607  lhop1lem  24609  lhop1  24610  lhop2  24611  lhop  24612  ftc1cn  24639  tdeglem4  24653  mdegleb  24657  mdegldg  24659  mdegaddle  24667  ply1remlem  24755  ply1rem  24756  fta1glem1  24758  fta1glem2  24759  fta1blem  24761  plyeq0lem  24799  plyeq0  24800  plyaddlem1  24802  coeeulem  24813  coeaddlem  24838  coemulc  24844  dgradd2  24857  dgrcolem2  24863  ofmulrt  24870  plyrem  24893  vieta1lem1  24898  vieta1  24900  plyexmo  24901  elqaalem3  24909  aannenlem1  24916  aalioulem2  24921  ulmuni  24979  ulmdvlem1  24987  ulmdv  24990  mbfulm  24993  iblulm  24994  itgulm  24995  rlimcnp2  25543  jensen  25565  amgm  25567  basellem3  25659  basellem7  25663  basellem9  25665  dchrelbas2  25812  dchrmulcl  25824  dchrfi  25830  dchreq  25833  dchrresb  25834  dchrinv  25836  dchr1re  25838  sumdchr2  25845  dchr2sum  25848  lgsqrlem2  25922  lgsqrlem3  25923  rpvmasum2  26087  dchrisum0re  26088  mirf1o  26454  lmif1o  26580  eqeefv  26688  axlowdimlem14  26740  vtxdgfisf  27257  2pthon3v  27721  nvinvfval  28416  sspg  28504  ssps  28506  sspmlem  28508  sspn  28512  lnon0  28574  ubthlem1  28646  pjfn  29485  kbpj  29732  kbass2  29893  elpjrn  29966  ofrn2  30386  off2  30387  ofresid  30388  xppreima2  30394  ofpreima2  30410  suppovss  30425  resf1o  30465  swrdrn3  30629  gsumle  30725  symgcom2  30728  pmtrcnel  30733  pmtrcnel2  30734  pmtrcnelor  30735  cycpmfvlem  30754  cycpmfv3  30757  cycpmcl  30758  cycpmco2rn  30767  cycpmco2  30775  cycpm3cl2  30778  cyc3co2  30782  cyc3evpm  30792  islinds5  30932  ellspds  30933  dimkerim  31023  fedgmullem2  31026  fedgmul  31027  cmpcref  31114  fsumcvg4  31193  pl1cn  31198  qqhval2lem  31222  prodindf  31282  indpreima  31284  esumcvg  31345  ofcf  31362  ofcof  31366  measfn  31463  meascnbl  31478  sibfof  31598  sitgaddlemb  31606  subiwrdlen  31644  rrvfn  31703  plymul02  31816  signsplypnf  31820  signsply0  31821  reprsuc  31886  reprdifc  31898  breprexplema  31901  circlemethhgt  31914  hgt750lemb  31927  f1resrcmplf1dlem  32359  pthhashvtx  32374  cvmopnlem  32525  cvmliftmolem1  32528  cvmliftlem10  32541  cvmlift2lem9a  32550  cvmlift2lem6  32555  cvmlift2lem12  32561  cvmliftphtlem  32564  cvmlift3lem9  32574  mrsubrn  32760  elmrsubrn  32767  elmsubrn  32775  msubrn  32776  mclsind  32817  mclsppslem  32830  mclspps  32831  iprodefisumlem  32972  matunitlindflem1  34887  poimirlem1  34892  poimirlem2  34893  poimirlem3  34894  poimirlem16  34907  poimirlem17  34908  poimirlem19  34910  poimirlem20  34911  poimirlem22  34913  poimirlem23  34914  poimirlem29  34920  poimirlem30  34921  poimirlem31  34922  poimir  34924  mblfinlem2  34929  itg2addnclem3  34944  itg2addnc  34945  itg2gt0cn  34946  ftc1cnnc  34965  ftc1anclem5  34970  ftc1anclem7  34972  ftc1anc  34974  sdclem2  35016  istotbnd3  35048  sstotbnd2  35051  isbnd3  35061  heibor1lem  35086  rrnmet  35106  grpokerinj  35170  isdrngo2  35235  lfl1  36205  lfladdcl  36206  lflvscl  36212  lkr0f  36229  lkrsc  36232  eqlkr2  36235  eqlkr3  36236  ldualvaddval  36266  ldualvsval  36273  tendoeq1  37899  frlmvscadiccat  39143  frlmsnic  39147  ismrcd1  39293  ismrcd2  39294  istopclsd  39295  isnacs3  39305  mzpaddmpt  39336  mzpmulmpt  39337  mzpsubst  39343  mzpcong  39567  fnwe2lem2  39649  islmodfg  39667  kercvrlsm  39681  dgrsub2  39733  mpaaeu  39748  rngunsnply  39771  idomrootle  39793  hausgraph  39810  fsovf1od  40360  brcoffn  40378  clsneiel1  40456  wfximgfd  40512  extoimad  40513  mnurndlem1  40615  caofcan  40653  ofmul12  40655  ofdivrec  40656  ofdivcan4  40657  ofdivdiv2  40658  dvconstbi  40664  binomcxplemnotnn0  40686  refsum2cnlem1  41292  ssmapsn  41477  preimaiocmnf  41835  fsumsupp0  41857  fsumsermpt  41858  climinf  41885  climinf2lem  41985  limsupmnflem  41999  limsupvaluz2  42017  supcnvlimsup  42019  limsupgtlem  42056  liminfvalxr  42062  liminflelimsupuz  42064  xlimconst2  42114  climxlim2  42125  icccncfext  42168  dvnprodlem1  42229  volicoff  42279  voliooicof  42280  fourierdlem25  42416  etransclem2  42520  etransclem35  42553  fge0iccico  42651  sge0tsms  42661  sge0sup  42672  sge0resrn  42685  sge0le  42688  sge0fodjrnlem  42697  sge0isum  42708  sge0seq  42727  nnfoctbdjlem  42736  meadjiunlem  42746  omeiunle  42798  hoicvr  42829  ovolval4lem1  42930  ovolval5lem3  42935  ovnovollem1  42937  ovnovollem2  42938  iinhoiicclem  42954  iunhoiioolem  42956  preimaicomnf  42989  smfresal  43062  smfsuplem1  43084  smflimsuplem2  43094  mgmhmf1o  44053  resmgmhm2b  44066  mgmhmima  44068  mgmhmeql  44069  rnghmf1o  44173  amgmwlem  44902