Theorem ffnd 6388

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

Syntax hints:   → wi 4   Fn wfn 6225  ⟶wf 6226

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 208  df-an 397  df-f 6234

This theorem is referenced by:  fnconstg  6440  f1fn  6449  fofn  6465  f1ofn  6489  feqmptd  6606  fprb  6828  rnmptc  6841  cocan1  6917  oprres  7177  off  7287  ofco  7292  caofref  7298  caofid0l  7300  caofid0r  7301  caofid1  7302  caofid2  7303  caofrss  7305  caoftrn  7307  fo2ndf  7675  fnwelem  7683  fnse  7685  suppss  7716  suppssr  7717  suppssof1  7719  suppofssd  7723  suppofss1d  7724  suppofss2d  7725  smorndom  7862  elmapfn  8284  ralxpmap  8314  omxpenlem  8470  mapen  8533  f1finf1o  8596  unirnffid  8667  fdmfifsupp  8694  mapfien  8722  intrnfi  8731  marypha2  8754  ordtypelem7  8839  wemapsolem  8865  wemapso  8866  wemapso2lem  8867  unxpwdom2  8903  ixpiunwdom  8906  cantnfle  8985  cantnfp1lem2  8993  cantnfp1lem3  8994  cantnfp1  8995  oemapvali  8998  cantnflem1a  8999  cantnflem1c  9001  cantnflem3  9005  cantnf  9007  cnfcomlem  9013  cnfcom3  9018  updjudhcoinlf  9212  updjudhcoinrg  9213  fseqenlem1  9301  numacn  9326  infpwfien  9339  isf32lem2  9627  isf34lem7  9652  isf34lem6  9653  unirnfdomd  9840  ofsubeq0  11488  ofnegsub  11489  ofsubge0  11490  seqf1olem2  13265  resunimafz0  13656  wrdfn  13727  swrdvalfn  13854  swrdccat2  13872  pfxfn  13884  pfxid  13887  cats1un  13924  cshwfn  14004  ccatco  14038  limsupgle  14673  o1of2  14808  o1rlimmul  14814  isercolllem2  14861  isercoll  14863  isercoll2  14864  climsup  14865  fsumss  14920  ruclem11  15431  vdwlem2  16152  vdwlem6  16156  vdwlem9  16159  vdwlem12  16162  0ram  16190  ramub1lem1  16196  pwsle  16599  pwsleval  16600  pwsvscaval  16602  mrcuni  16726  mrcun  16727  invf1o  16873  funcres2c  17005  setcmon  17181  setcepi  17182  uncfcurf  17323  yoniso  17369  isacs4lem  17612  acsmapd  17622  gsumval2  17724  prdsplusgcl  17765  prdsidlem  17766  prdsmndd  17767  mhmf1o  17789  resmhm2b  17805  mhmima  17807  mhmeql  17808  prdspjmhm  17811  pwsco1mhm  17814  pwsco2mhm  17815  gsumwmhm  17826  frmdss2  17844  grpinvf1o  17931  prdsinvlem  17970  cycsubgcl  18064  ghmrn  18117  ghmpreima  18126  ghmeql  18127  ghmnsgima  18128  ghmnsgpreima  18129  ghmeqker  18131  ghmf1o  18134  gass  18177  cntzmhm  18215  symgextres  18289  gsmsymgrfixlem1  18291  fvcosymgeq  18293  f1omvdconj  18310  pmtrfinv  18325  symgtrinv  18336  pmtr3ncomlem1  18337  sygbasnfpfi  18376  efgredleme  18601  ghmplusg  18694  prdscmnd  18709  gsumval3a  18749  gsumval3eu  18750  gsumzaddlem  18766  gsumzsplit  18772  gsumpt  18807  prdsgsum  18823  dprdfcntz  18859  dprdfadd  18864  dprdfeq0  18866  dprdf11  18867  dprdlub  18870  dprdspan  18871  dprd2dlem1  18885  dmdprdpr  18893  dprdpr  18894  dpjlem  18895  ablfac1eu  18917  prdsmulrcl  19056  prdsringd  19057  prdscrngd  19058  prds1  19059  rhmf1o  19179  rnrhmsubrg  19262  isabvd  19286  lmodfopnelem1  19365  lcomfsupp  19369  prdsvscacl  19435  prdslmodd  19436  lmhmco  19510  lmhmplusg  19511  lmhmvsca  19512  lmhmf1o  19513  lmhmeql  19522  lspextmo  19523  rrgsupp  19758  psrbaglesupp  19841  psrbagcon  19844  psrbaglefi  19845  psrbagconf1o  19847  gsumbagdiaglem  19848  psrvscaval  19865  psrlidm  19876  psrridm  19877  psrass1  19878  psrdi  19879  psrdir  19880  mplsubglem  19907  mplvscaval  19921  subrgmvrf  19935  mplbas2  19943  mvrf2  19964  mplind  19974  psrbagev1  19982  evlslem3  19986  evlslem1  19987  evlsvar  19995  mpfind  20008  mhpinvcl  20027  psrplusgpropd  20092  coe1add  20120  coe1addfv  20121  evl1addd  20191  evl1subd  20192  evl1muld  20193  pf1mpf  20202  pf1ind  20205  pjfo  20546  dsmmbas2  20568  dsmm0cl  20571  dsmmacl  20572  dsmmsubg  20574  dsmmlss  20575  frlmvplusgvalc  20598  frlmvscaval  20599  frlmplusgvalb  20600  frlmvscavalb  20601  frlmsslss2  20606  frlmphllem  20611  frlmphl  20612  frlmssuvc2  20626  frlmsslsp  20627  frlmup1  20629  frlmup2  20630  frlmup3  20631  frlmup4  20632  islindf4  20669  mamudir  20702  mamulid  20739  mamurid  20740  mdetrlin  20900  mdetrsca  20901  mdetralt  20906  mdetunilem7  20916  mdetunilem9  20918  madurid  20942  cnrest2  21583  lmss  21595  lmcnp  21601  cnt0  21643  cnt1  21647  cnhaus  21651  rncmp  21693  conncn  21723  2ndcomap  21755  1stccnp  21759  comppfsc  21829  1stckgenlem  21850  ptbasfi  21878  ptopn  21880  ptclsg  21912  ptcnp  21919  upxp  21920  txtube  21937  txcmplem1  21938  hauseqlcld  21943  xkohaus  21950  xkoptsub  21951  cnmpt11  21960  cnmpt21  21968  cnmpt22f  21972  cnmptcom  21975  qtopss  22012  qtopeu  22013  qtopomap  22015  qtopcmap  22016  kqffn  22022  hmeof1o2  22060  xkocnv  22111  rnelfm  22250  ptcmplem1  22349  cnextfres1  22365  ghmcnp  22411  tgphaus  22413  prdstmdd  22420  prdstgpd  22421  fmucnd  22589  psmetxrge0  22611  isxmet2d  22625  prdsmet  22668  blelrnps  22714  blelrn  22715  xmetresbl  22735  comet  22811  stdbdxmet  22813  met2ndci  22820  prdsxmslem2  22827  isngp3  22895  nmotri  23036  metdsre  23149  bndth  23250  evth  23251  fmcfil  23563  bcthlem4  23618  rrxcph  23683  rrxds  23684  rrxmet  23699  evthicc2  23749  ovolfsf  23760  ovolmge0  23766  ovollb2lem  23777  ovolunlem1a  23785  ovoliunlem1  23791  ovoliun  23794  ovoliun2  23795  ovolscalem1  23802  ovolicc1  23805  ovolicc2lem4  23809  ovolicc2  23811  voliunlem1  23839  voliunlem3  23841  volsup  23845  ioombl1lem2  23848  ioombl1lem4  23850  uniiccdif  23867  uniioombllem2  23872  uniioombllem3  23874  uniioombllem6  23877  volsup2  23894  vitalilem4  23900  mbfeqalem1  23930  mbfmulc2lem  23936  mbfmax  23938  mbfaddlem  23949  mbfadd  23950  mbfsub  23951  mbfsup  23953  mbfinf  23954  itg1ge0  23975  itg1addlem1  23981  i1faddlem  23982  i1fmullem  23983  i1fadd  23984  i1fmul  23985  itg1addlem4  23988  i1fmulclem  23991  i1fmulc  23992  itg1mulc  23993  i1fres  23994  itg10a  23999  itg1ge0a  24000  itg1lea  24001  mbfi1fseqlem3  24006  mbfi1fseqlem4  24007  mbfi1flimlem  24011  mbfmullem2  24013  mbfmul  24015  itg20  24026  itg2lea  24033  itg2splitlem  24037  itg2split  24038  itg2monolem1  24039  itg2monolem2  24040  itg2monolem3  24041  itg2mono  24042  itg2i1fseqle  24043  itg2i1fseq  24044  itg2addlem  24047  itg2gt0  24049  itg2cnlem1  24050  itg2cnlem2  24051  itg2cn  24052  itgitg1  24097  bddmulibl  24127  bddibl  24128  dvidlem  24201  dvaddbr  24223  dvmulbr  24224  dvaddf  24227  dvcmulf  24230  dvrec  24240  dvcnvlem  24261  rolle  24275  dveq0  24285  dv11cn  24286  dvivthlem2  24294  dvivth  24295  dvne0  24296  lhop1lem  24298  lhop1  24299  lhop2  24300  lhop  24301  ftc1cn  24328  tdeglem4  24342  mdegleb  24346  mdegldg  24348  mdegaddle  24356  ply1remlem  24444  ply1rem  24445  fta1glem1  24447  fta1glem2  24448  fta1blem  24450  plyeq0lem  24488  plyeq0  24489  plyaddlem1  24491  coeeulem  24502  coeaddlem  24527  coemulc  24533  dgradd2  24546  dgrcolem2  24552  ofmulrt  24559  plyrem  24582  vieta1lem1  24587  vieta1  24589  plyexmo  24590  elqaalem3  24598  aannenlem1  24605  aalioulem2  24610  ulmuni  24668  ulmdvlem1  24676  ulmdv  24679  mbfulm  24682  iblulm  24683  itgulm  24684  rlimcnp2  25231  jensen  25253  amgm  25255  basellem3  25347  basellem7  25351  basellem9  25353  dchrelbas2  25500  dchrmulcl  25512  dchrfi  25518  dchreq  25521  dchrresb  25522  dchrinv  25524  dchr1re  25526  sumdchr2  25533  dchr2sum  25536  lgsqrlem2  25610  lgsqrlem3  25611  rpvmasum2  25775  dchrisum0re  25776  mirf1o  26142  lmif1o  26268  eqeefv  26377  axlowdimlem14  26429  vtxdgfisf  26946  2pthon3v  27414  nvinvfval  28113  sspg  28201  ssps  28203  sspmlem  28205  sspn  28209  lnon0  28271  ubthlem1  28343  pjfn  29182  kbpj  29429  kbass2  29590  elpjrn  29663  ofrn2  30082  off2  30083  ofresid  30084  xppreima2  30090  ofpreima2  30106  suppovss  30121  resf1o  30159  symgcom2  30392  pmtrcnel  30397  pmtrcnel2  30398  pmtrcnelor  30399  cycpmfvlem  30406  cycpmfv3  30409  cycpmcl  30410  cycpm3cl2  30420  cyc3co2  30424  cyc3evpm  30435  gsumle  30499  islinds5  30585  ellspds  30586  dimkerim  30632  fedgmullem2  30635  fedgmul  30636  cmpcref  30736  fsumcvg4  30815  pl1cn  30820  qqhval2lem  30844  prodindf  30904  indpreima  30906  esumcvg  30967  ofcf  30984  ofcof  30988  measfn  31085  meascnbl  31100  sibfof  31220  sitgaddlemb  31228  subiwrdlen  31266  rrvfn  31325  plymul02  31438  signsplypnf  31442  signsply0  31443  reprsuc  31508  reprdifc  31520  breprexplema  31523  circlemethhgt  31536  hgt750lemb  31549  f1resrcmplf1dlem  31978  pthhashvtx  31988  cvmopnlem  32139  cvmliftmolem1  32142  cvmliftlem10  32155  cvmlift2lem9a  32164  cvmlift2lem6  32169  cvmlift2lem12  32175  cvmliftphtlem  32178  cvmlift3lem9  32188  mrsubrn  32374  elmrsubrn  32381  elmsubrn  32389  msubrn  32390  mclsind  32431  mclsppslem  32444  mclspps  32445  iprodefisumlem  32586  matunitlindflem1  34444  poimirlem1  34449  poimirlem2  34450  poimirlem3  34451  poimirlem16  34464  poimirlem17  34465  poimirlem19  34467  poimirlem20  34468  poimirlem22  34470  poimirlem23  34471  poimirlem29  34477  poimirlem30  34478  poimirlem31  34479  poimir  34481  mblfinlem2  34486  itg2addnclem3  34501  itg2addnc  34502  itg2gt0cn  34503  ftc1cnnc  34522  ftc1anclem5  34527  ftc1anclem7  34529  ftc1anc  34531  sdclem2  34574  istotbnd3  34606  sstotbnd2  34609  isbnd3  34619  heibor1lem  34644  rrnmet  34664  grpokerinj  34728  isdrngo2  34793  lfl1  35762  lfladdcl  35763  lflvscl  35769  lkr0f  35786  lkrsc  35789  eqlkr2  35792  eqlkr3  35793  ldualvaddval  35823  ldualvsval  35830  tendoeq1  37456  frlmvscadiccat  38697  frlmsnic  38701  ismrcd1  38805  ismrcd2  38806  istopclsd  38807  isnacs3  38817  mzpaddmpt  38848  mzpmulmpt  38849  mzpsubst  38855  mzpcong  39079  fnwe2lem2  39161  islmodfg  39179  kercvrlsm  39193  dgrsub2  39245  mpaaeu  39260  rngunsnply  39283  idomrootle  39305  hausgraph  39322  fsovf1od  39872  brcoffn  39890  clsneiel1  39968  wfximgfd  40024  extoimad  40025  mnurndlem1  40139  caofcan  40218  ofmul12  40220  ofdivrec  40221  ofdivcan4  40222  ofdivdiv2  40223  dvconstbi  40229  binomcxplemnotnn0  40251  refsum2cnlem1  40858  ssmapsn  41044  preimaiocmnf  41404  fsumsupp0  41426  fsumsermpt  41427  climinf  41454  climinf2lem  41554  limsupmnflem  41568  limsupvaluz2  41586  supcnvlimsup  41588  limsupgtlem  41625  liminfvalxr  41631  liminflelimsupuz  41633  xlimconst2  41683  climxlim2  41694  icccncfext  41737  dvnprodlem1  41798  volicoff  41848  voliooicof  41849  fourierdlem25  41985  etransclem2  42089  etransclem35  42122  fge0iccico  42220  sge0tsms  42230  sge0sup  42241  sge0resrn  42254  sge0le  42257  sge0fodjrnlem  42266  sge0isum  42277  sge0seq  42296  nnfoctbdjlem  42305  meadjiunlem  42315  omeiunle  42367  hoicvr  42398  ovolval4lem1  42499  ovolval5lem3  42504  ovnovollem1  42506  ovnovollem2  42507  iinhoiicclem  42523  iunhoiioolem  42525  preimaicomnf  42558  smfresal  42631  smfsuplem1  42653  smflimsuplem2  42663  mgmhmf1o  43562  resmgmhm2b  43575  mgmhmima  43577  mgmhmeql  43578  rnghmf1o  43678  amgmwlem  44409