Theorem ffn 6705

Description: A mapping is a function with domain. (Contributed by NM, 2-Aug-1994.)

Assertion

Ref	Expression
ffn	⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴)

Proof of Theorem ffn

Step	Hyp	Ref	Expression
1		df-f 6534	. 2 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
2	1	simplbi 497	1 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴)

Syntax hints:   → wi 4   ⊆ wss 3926  ran crn 5655   Fn wfn 6525  ⟶wf 6526

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 6534

This theorem is referenced by:  ffnd  6706  ffun  6708  frel  6710  fdm  6714  ffrn  6718  fresin  6746  fresaun  6748  fresaunres2  6749  fcoi1  6751  feu  6753  f0bi  6760  dffo2  6793  fimadmfo  6798  fdmeu  6934  feqmptdf  6948  fimarab  6952  fvco3  6977  ffvelcdm  7070  dff2  7088  dffo3  7091  dffo4  7092  dffo5  7093  dffo3f  7095  f1ompt  7100  ffnfv  7108  fcdmssb  7111  fcompt  7122  fsn2  7125  fprb  7185  fconst2g  7194  fpr2g  7202  fex  7217  dff13  7246  nvocnv  7273  soisores  7319  fdmexb  7901  resf1extb  7928  fo1stres  8012  fo2ndres  8013  1stcof  8016  2ndcof  8017  curry1f  8103  curry2f  8105  fparlem1  8109  fparlem2  8110  fo2ndf  8118  soseq  8156  tposf2  8247  smo11  8376  fsetexb  8876  mapsnd  8898  pw2f1olem  9088  mapen  9153  mapunen  9158  fissuni  9367  fipreima  9368  indexfi  9370  mapfien  9418  oismo  9552  cantnflt  9684  cantnfp1lem3  9692  cantnflem4  9704  tcrank  9896  updjudhcoinlf  9944  updjudhcoinrg  9945  updjud  9946  infpwfien  10074  cardinfima  10109  dfacacn  10154  cfflb  10271  cofsmo  10281  cfcoflem  10284  coftr  10285  fin23lem40  10363  axdc3lem2  10463  ac6num  10491  ac6c4  10493  ac6s2  10498  ttukeylem6  10526  iunfo  10551  pwcfsdom  10595  fpwwe2lem5  10647  fpwwe2lem7  10649  pwfseqlem3  10672  inar1  10787  tskcard  10793  tskuni  10795  tskurn  10801  gruima  10814  nqerrel  10944  recmulnq  10976  dmrecnq  10980  axpre-sup  11181  ofsubeq0  12235  dfz2  12605  uzn0  12867  rpnnen1lem3  12993  rpnnen1lem5  12995  unirnioo  13464  dfioo2  13465  ioorebas  13466  fseq1p1m1  13613  2ffzeq  13664  fvinim0ffz  13800  injresinjlem  13801  fsequb2  13992  fseqsupcl  13993  fseqsupubi  13994  ser0f  14071  hashgval  14349  hashinf  14351  hashresfn  14356  ffz0hash  14463  fnfzo0hash  14466  wrdred1hash  14577  revlen  14778  revrev  14783  repswlen  14792  repsdf2  14794  cshword  14807  0csh0  14809  lenco  14849  s1co  14850  cshco  14853  swrdco  14854  s7f1o  14983  ofccat  14986  shftf  15096  uzin2  15361  rexanuz  15362  limsuple  15492  limsupval2  15494  rlimres  15572  lo1res  15573  rlimresb  15579  isercolllem2  15680  isercolllem3  15681  isercoll  15682  supcvg  15870  prodf1f  15906  eff2  16115  reeff1  16136  tanval  16144  ruclem4  16250  ruclem12  16257  prmreclem6  16939  1arithlem4  16944  1arith  16945  vdwmc  16996  vdwlem1  16999  vdwlem8  17006  vdwlem13  17011  ramval  17026  0ram  17038  0ram2  17039  0ramcl  17041  ramcl  17047  fsets  17186  firest  17444  0ssc  17848  0subcat  17849  isfull2  17924  arwhoma  18056  gsumval2a  18661  isgrpinv  18974  kerf1ghm  19228  f1omvdconj  19425  pmtrmvd  19435  pmtrfinv  19440  pmtrdifellem4  19458  efgsfo  19718  efgredlem  19726  efgcpbllemb  19734  frgpup3lem  19756  0frgp  19758  gexex  19832  torsubg  19833  gsumval3  19886  gsumzres  19888  gsummptmhm  19919  gsumzoppg  19923  dprdf1o  20013  dprd2db  20024  zrinitorngc  20600  zrtermorngc  20601  zrtermoringc  20633  srngf1o  20806  lmhmima  21003  lmhmpreima  21004  lmhmrnlss  21006  lspextmo  21012  pwssplit1  21015  cnfldadd  21319  cnfldmul  21321  dfcnfldOLD  21329  cnfldplusf  21357  cnfldsub  21358  chrrhm  21490  znunit  21522  psgnevpmb  21545  psgndiflemB  21558  mpofrlmd  21735  frlmipval  21737  frlmphl  21739  frlmlbs  21755  frlmup4  21759  ellspd  21760  lindfmm  21785  lsslindf  21788  psrbaglefi  21884  psrlidm  21920  mplmonmul  21992  evlseu  22039  mpfconst  22057  mpfproj  22058  mpfsubrg  22059  coe1sclmulfv  22218  pf1const  22282  pf1id  22283  pf1subrg  22284  mpfpf1  22287  pf1mpf  22288  mamuass  22338  mamudi  22339  mamudir  22340  mamuvs1  22341  mamuvs2  22342  1mavmul  22484  mavmulass  22485  mdetunilem7  22554  madutpos  22578  lecldbas  23155  lmbr2  23195  cncnpi  23214  cncnp  23216  cnpdis  23229  lmff  23237  pnrmopn  23279  dnsconst  23314  cmpsub  23336  tgcmp  23337  hauscmplem  23342  2ndcctbss  23391  2ndcomap  23394  2ndcsep  23395  1stccnp  23398  kgenidm  23483  iskgen2  23484  1stckgen  23490  kgen2cn  23495  ptpjpre1  23507  pttop  23518  ptuni  23530  ptval2  23537  tx1cn  23545  tx2cn  23546  ptpjcn  23547  ptpjopn  23548  ptclsg  23551  ptcnplem  23557  upxp  23559  txcnmpt  23560  uptx  23561  txcmplem2  23578  txkgen  23588  xkoptsub  23590  xkopt  23591  xkococnlem  23595  xkococn  23596  ptcmpfi  23749  zfbas  23832  uzrest  23833  rnelfmlem  23888  rnelfm  23889  fmfnfmlem2  23891  fmfnfm  23894  lmflf  23941  alexsubALT  23987  clssubg  24045  qustgplem  24057  tsmsres  24080  tsmsxplem1  24089  ucncn  24221  xmettpos  24286  imasdsf1olem  24310  blrnps  24345  blrn  24346  xmeterval  24369  tmslem  24419  tmsxms  24423  imasf1oxms  24426  prdsxms  24467  blval2  24499  metuel2  24502  isngp2  24534  isngp3  24535  tngngp2  24589  isnghm  24660  qtopbaslem  24695  qdensere  24706  cnbl0  24710  cnblcld  24711  cnfldms  24712  blssioo  24732  tgioo  24733  tgqioo  24737  xrtgioo  24744  xrsdsre  24748  xrge0tsms  24772  iimulcnOLD  24884  bndth  24906  lebnumlem3  24911  nmhmcn  25069  cphsqrtcl  25134  lmmbr2  25209  caucfil  25233  causs  25248  lmcau  25263  bcth3  25281  cncms  25305  cnfldcusp  25307  rrxmvallem  25354  ivthicc  25409  ovolfioo  25418  ovolficc  25419  ovolficcss  25420  ovollb2lem  25439  ovoliunlem2  25454  ovolshftlem1  25460  ovolicc2  25473  ismbl  25477  voliunlem2  25502  volsup  25507  ioorf  25524  ioorinv  25527  ioorcl  25528  uniiccdif  25529  uniioovol  25530  uniiccvol  25531  uniioombllem2  25534  uniioombllem4  25537  dyaddisj  25547  dyadmax  25549  dyadmbllem  25550  dyadmbl  25551  opnmbllem  25552  opnmblALT  25554  volsup2  25556  mbfdm  25577  mbfima  25581  mbfid  25586  ismbfd  25590  mbfres2  25596  mbfposr  25603  mbfimaopnlem  25606  mbflimsup  25617  0plef  25623  i1f1lem  25640  itg11  25642  itg1addlem4  25650  i1fpos  25657  itg1le  25664  itg1climres  25665  mbfi1fseqlem5  25670  mbfi1flimlem  25673  xrge0f  25682  itg2ge0  25686  itg2seq  25693  itg2i1fseqle  25705  itg2i1fseq2  25707  itg2addlem  25709  itg2gt0  25711  limciun  25845  dvres  25862  dvres3a  25865  cpnres  25889  dvfre  25905  dvmptres3  25910  dvlip2  25950  dvgt0lem2  25958  deg1fvi  26040  uc1pmon1p  26107  fta1g  26125  ig1peu  26130  ig1pdvds  26135  plyco0  26147  plypf1  26167  dgrlem  26184  dgrub  26189  dgrlb  26191  coemulc  26210  plyreres  26240  plydivlem3  26253  plydivlem4  26254  plydiveu  26256  plyremlem  26262  fta1lem  26265  fta1  26266  vieta1lem2  26269  plyexmo  26271  elaa  26274  elqaalem3  26279  aannenlem1  26286  pserulm  26381  psercnlem2  26384  psercnlem1  26385  psercn  26386  abelth  26401  reeff1o  26407  pilem1  26411  recosf1o  26494  resinf1o  26495  efif1olem3  26503  efif1olem4  26504  efifo  26506  eff1olem  26507  ellogrn  26518  logcn  26606  dvloglem  26607  logf1o2  26609  efopnlem1  26615  efopnlem2  26616  efopn  26617  logtayl  26619  cxpcn3lem  26707  cxpcn3  26708  resqrtcn  26709  asinneg  26846  areambl  26918  emcllem7  26962  lgamgulm2  26996  basellem4  27044  sqff1o  27142  mpodvdsmulf1o  27154  fsumdvdsmul  27155  dvdsmulf1o  27156  fsumdvdsmulOLD  27157  ostthlem1  27588  ostth  27600  noetasuplem4  27698  madeval2  27809  elold  27825  old1  27831  madeoldsuc  27840  tglnfn  28472  f1otrg  28796  axlowdimlem6  28872  axlowdimlem8  28874  axlowdimlem9  28875  axlowdimlem11  28877  axlowdimlem12  28878  axlowdimlem17  28883  elntg2  28910  dfpth2  29657  cyclnumvtx  29728  crctcshlem4  29748  clwlkclwwlklem2  29927  eucrct2eupth  30172  ex-fpar  30389  cnnvm  30609  sspmlem  30659  nvo00  30688  nmlno0lem  30720  phoeqi  30784  ubthlem1  30797  hhip  31104  hhssabloilem  31188  hhssnv  31191  hhsssh  31196  occllem  31230  shsel  31241  chscllem2  31565  df0op2  31679  hoeq  31687  hocofni  31694  hoaddfni  31697  hosubfni  31698  hon0  31720  ho01i  31755  hoeq1  31757  elnlfn  31855  nmlnop0iALT  31922  lnopco0i  31931  imaelshi  31985  nlelchi  31988  rnbra  32034  cnvbraval  32037  kbass5  32047  hmopidmchi  32078  hmopidmpji  32079  foresf1o  32431  fcomptf  32582  ofpreima  32589  resf1o  32653  maprnin  32654  fpwrelmapffslem  32655  hashgt1  32733  indpi1  32783  indpreima  32788  s3clhash  32869  gsumpart  32997  xrge0tsmsd  33002  tocyc01  33075  cyc3evpm  33107  cycpmgcl  33110  cycpmconjslem2  33112  cyc3conja  33114  kerunit  33287  1arithidomlem1  33496  1arithidomlem2  33497  1arithidom  33498  dimval  33586  dimvalfi  33587  ply1degltdimlem  33608  ply1degltdim  33609  elirng  33673  txomap  33811  locfinreflem  33817  hauseqcn  33875  xpinpreima  33883  xpinpreima2  33884  tpr2rico  33889  mndpluscn  33903  raddcn  33906  xrge0pluscn  33917  xrge0tmdALT  33923  rge0scvg  33926  pl1cn  33932  elzrhunit  33954  qqhf  33963  cnrrext  33987  qqhre  33997  1stmbfm  34238  2ndmbfm  34239  mbfmcnt  34246  omssubadd  34278  carsggect  34296  eulerpartlemsv2  34336  eulerpartlems  34338  eulerpartlemv  34342  eulerpartlemb  34346  eulerpartlemf  34348  eulerpartlemt  34349  eulerpartlemmf  34353  eulerpartlemgvv  34354  eulerpartlemgh  34356  eulerpartlemgs2  34358  sseqmw  34369  sseqf  34370  sseqp1  34373  fiblem  34376  fibp1  34379  plymul02  34524  signsvtn0  34548  signstres  34553  signshlen  34568  reprinrn  34596  circlemethhgt  34621  txsconnlem  35208  iccllysconn  35218  rellysconn  35219  cvmseu  35244  cvmliftmolem2  35250  cvmliftlem6  35258  cvmliftlem7  35259  cvmliftlem8  35260  cvmliftlem9  35261  cvmliftlem11  35263  cvmliftlem15  35266  cvmlift2lem7  35277  cvmlift2lem10  35280  cvmlift3lem8  35294  cvmlift3lem9  35295  mvrsfpw  35474  mrsubff1  35482  msrid  35513  msrfo  35514  elmsta  35516  mtyf  35520  msubff1  35524  vhmcls  35534  mclsax  35537  elmthm  35544  mthmblem  35548  mclsppslem  35551  iprodefisumlem  35703  fullfunfnv  35910  fullfunfv  35911  tailfb  36341  filnetlem4  36345  taupilem3  37283  icoreresf  37316  icoreelrnab  37318  relowlssretop  37327  relowlpssretop  37328  unccur  37573  matunitlindflem1  37586  matunitlindflem2  37587  ptrecube  37590  poimirlem28  37618  poimirlem32  37622  heicant  37625  opnmbllem0  37626  mblfinlem1  37627  mblfinlem2  37628  volsupnfl  37635  cnambfre  37638  dvtan  37640  itg2addnclem  37641  itg2addnclem2  37642  ftc1anclem3  37665  ftc1anclem5  37667  ftc1anclem7  37669  ftc1anclem8  37670  ftc1anc  37671  areacirc  37683  indexdom  37704  sdclem2  37712  sstotbnd2  37744  sstotbnd  37745  isbndx  37752  isbnd3b  37755  prdsbnd  37763  prdstotbnd  37764  ismtyhmeolem  37774  heibor1lem  37779  heiborlem1  37781  heibor  37791  rrnequiv  37805  keridl  38002  ellkr  39053  lkr0f  39058  cdleme50rnlem  40509  aks6d1c2lem4  42086  aks6d1c5  42098  sticksstones11  42115  sticksstones19  42124  sticksstones22  42127  aks6d1c6lem4  42132  aks6d1c6isolem2  42134  fsuppind  42560  elrfirn  42665  ismrcd2  42669  isnacs2  42676  nacsfix  42682  mapfzcons1  42687  mzpcompact2lem  42721  eq0rabdioph  42746  eldioph4b  42781  diophren  42783  pw2f1ocnv  43008  pw2f1o2val2  43011  lmhmfgsplit  43057  pwssplit4  43060  hbt  43101  mpaaeu  43121  mendring  43159  proot1mul  43165  proot1hash  43166  proot1ex  43167  deg1mhm  43171  fgraphopab  43174  hausgraph  43176  nvocnvb  43393  ofsubid  44296  expgrowthi  44305  expgrowth  44307  binomcxplemdvbinom  44325  binomcxplemcvg  44326  binomcxplemnotnn0  44328  relpfrlem  44926  rfcnpre1  44991  rfcnpre2  45003  cncmpmax  45004  rfcnpre3  45005  rfcnpre4  45006  elixpconstg  45061  ffi  45145  islptre  45596  resincncf  45852  dvcosre  45889  dvresntr  45895  volioof  45964  stoweidlem48  46025  fourierdlem12  46096  fourierdlem15  46099  fourierdlem41  46125  fourierdlem42  46126  fourierdlem46  46129  fourierdlem48  46131  fourierdlem49  46132  fourierdlem54  46137  fourierdlem56  46139  fourierdlem62  46145  fourierdlem64  46147  fourierdlem65  46148  fourierdlem73  46156  fourierdlem74  46157  fourierdlem75  46158  fourierdlem102  46185  fourierdlem103  46186  fourierdlem104  46187  fourierdlem114  46197  sge0split  46386  elhoi  46519  mbfresmf  46716  cfsetsnfsetf1  47036  cfsetsnfsetfo  47037  focofob  47057  f1ocof1ob  47058  fafvelcdm  47147  ffnafv  47148  fafv2elcdm  47211  fafv2elrnb  47212  imarnf1pr  47259  2ffzoeq  47304  fundcmpsurbijinjpreimafv  47369  fundcmpsurinjimaid  47373  fargshiftfv  47401  fargshiftf  47402  fargshiftf1  47403  fargshiftfo  47404  cycl3grtri  47907  fdmdifeqresdif  48265  fdivmpt  48468  fdivmptf  48469  refdivmptf  48470  1arymaptf1  48570  2arymaptf1  48581  ackfnnn0  48613  homf0  48932  aacllem  49613