Theorem ffn 6630

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 6462	. 2 ⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))
2	1	simplbi 498	1 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴)

Syntax hints:   → wi 4   ⊆ wss 3891  ran crn 5601   Fn wfn 6453  ⟶wf 6454

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 206  df-an 397  df-f 6462

This theorem is referenced by:  ffnd  6631  ffun  6633  frel  6635  fdm  6639  fdmOLD  6640  ffrn  6644  fresin  6673  fresaun  6675  fresaunres2  6676  fcoi1  6678  feu  6680  f0bi  6687  dffo2  6722  fimadmfo  6727  feqmptdf  6871  fvco3  6899  ffvelcdm  6991  dff2  7007  dffo3  7010  dffo4  7011  dffo5  7012  f1ompt  7017  ffnfv  7024  fcdmssb  7027  fcompt  7037  fsn2  7040  fprb  7101  fconst2g  7110  fpr2g  7119  fex  7134  dff13  7160  nvocnv  7185  soisores  7230  fdmexb  7792  fo1stres  7893  fo2ndres  7894  1stcof  7897  2ndcof  7898  curry1f  7982  curry2f  7984  fparlem1  7988  fparlem2  7989  fo2ndf  7997  tposf2  8101  smo11  8230  fsetexb  8688  mapsnd  8710  pw2f1olem  8906  mapen  8971  mapunen  8976  fissuni  9182  fipreima  9183  indexfi  9185  mapfien  9225  oismo  9357  cantnflt  9488  cantnfp1lem3  9496  cantnflem4  9508  tcrank  9700  updjudhcoinlf  9748  updjudhcoinrg  9749  updjud  9750  infpwfien  9878  cardinfima  9913  dfacacn  9957  cfflb  10075  cofsmo  10085  cfcoflem  10088  coftr  10089  fin23lem40  10167  axdc3lem2  10267  ac6num  10295  ac6c4  10297  ac6s2  10302  ttukeylem6  10330  iunfo  10355  pwcfsdom  10399  fpwwe2lem5  10451  fpwwe2lem7  10453  pwfseqlem3  10476  inar1  10591  tskcard  10597  tskuni  10599  tskurn  10605  gruima  10618  nqerrel  10748  recmulnq  10780  dmrecnq  10784  axpre-sup  10985  ofsubeq0  12030  dfz2  12398  uzn0  12659  rpnnen1lem3  12779  rpnnen1lem5  12781  unirnioo  13241  dfioo2  13242  ioorebas  13243  fseq1p1m1  13390  2ffzeq  13437  fvinim0ffz  13566  injresinjlem  13567  fsequb2  13756  fseqsupcl  13757  fseqsupubi  13758  ser0f  13836  hashgval  14107  hashinf  14109  hashresfn  14114  ffz0hash  14218  fnfzo0hash  14221  wrdred1hash  14323  revlen  14534  revrev  14539  repswlen  14548  repsdf2  14550  cshword  14563  0csh0  14565  lenco  14604  s1co  14605  cshco  14608  swrdco  14609  ofccat  14739  shftf  14849  uzin2  15115  rexanuz  15116  limsuple  15246  limsupval2  15248  rlimres  15326  lo1res  15327  rlimresb  15333  isercolllem2  15436  isercolllem3  15437  isercoll  15438  supcvg  15627  prodf1f  15663  eff2  15867  reeff1  15888  tanval  15896  ruclem4  16002  ruclem12  16009  prmreclem6  16681  1arithlem4  16686  1arith  16687  vdwmc  16738  vdwlem1  16741  vdwlem8  16748  vdwlem13  16753  ramval  16768  0ram  16780  0ram2  16781  0ramcl  16783  ramcl  16789  fsets  16929  firest  17202  0ssc  17611  0subcat  17612  isfull2  17686  arwhoma  17819  gsumval2a  18428  isgrpinv  18691  f1omvdconj  19113  pmtrmvd  19123  pmtrfinv  19128  pmtrdifellem4  19146  efgsfo  19404  efgredlem  19412  efgcpbllemb  19420  frgpup3lem  19442  0frgp  19444  gexex  19513  torsubg  19514  gsumval3  19567  gsumzres  19569  gsummptmhm  19600  gsumzoppg  19604  dprdf1o  19694  dprd2db  19705  kerf1ghm  20046  srngf1o  20177  lmhmima  20372  lmhmpreima  20373  lmhmrnlss  20375  lspextmo  20381  pwssplit1  20384  cnfldplusf  20688  cnfldsub  20689  chrrhm  20798  znunit  20834  psgnevpmb  20855  psgndiflemB  20868  mpofrlmd  21047  frlmipval  21049  frlmphl  21051  frlmlbs  21067  frlmup4  21071  ellspd  21072  lindfmm  21097  lsslindf  21100  psrbaglefi  21198  psrbaglefiOLD  21199  psrlidm  21235  mplmonmul  21300  evlseu  21356  mpfconst  21374  mpfproj  21375  mpfsubrg  21376  coe1sclmulfv  21517  pf1const  21575  pf1id  21576  pf1subrg  21577  mpfpf1  21580  pf1mpf  21581  mamuass  21612  mamudi  21613  mamudir  21614  mamuvs1  21615  mamuvs2  21616  1mavmul  21760  mavmulass  21761  mdetunilem7  21830  madutpos  21854  lecldbas  22433  lmbr2  22473  cncnpi  22492  cncnp  22494  cnpdis  22507  lmff  22515  pnrmopn  22557  dnsconst  22592  cmpsub  22614  tgcmp  22615  hauscmplem  22620  2ndcctbss  22669  2ndcomap  22672  2ndcsep  22673  1stccnp  22676  kgenidm  22761  iskgen2  22762  1stckgen  22768  kgen2cn  22773  ptpjpre1  22785  pttop  22796  ptuni  22808  ptval2  22815  tx1cn  22823  tx2cn  22824  ptpjcn  22825  ptpjopn  22826  ptclsg  22829  ptcnplem  22835  upxp  22837  txcnmpt  22838  uptx  22839  txcmplem2  22856  txkgen  22866  xkoptsub  22868  xkopt  22869  xkococnlem  22873  xkococn  22874  ptcmpfi  23027  zfbas  23110  uzrest  23111  rnelfmlem  23166  rnelfm  23167  fmfnfmlem2  23169  fmfnfm  23172  lmflf  23219  alexsubALT  23265  clssubg  23323  qustgplem  23335  tsmsres  23358  tsmsxplem1  23367  ucncn  23500  xmettpos  23565  imasdsf1olem  23589  blrnps  23624  blrn  23625  xmeterval  23648  tmslem  23700  tmslemOLD  23701  tmsxms  23705  imasf1oxms  23708  prdsxms  23749  blval2  23781  metuel2  23784  isngp2  23816  isngp3  23817  tngngp2  23879  isnghm  23950  qtopbaslem  23985  qdensere  23996  cnbl0  24000  cnblcld  24001  cnfldms  24002  blssioo  24021  tgioo  24022  tgqioo  24026  xrtgioo  24032  xrsdsre  24036  xrge0tsms  24060  iimulcn  24164  bndth  24184  lebnumlem3  24189  nmhmcn  24346  cphsqrtcl  24411  lmmbr2  24486  caucfil  24510  causs  24525  lmcau  24540  bcth3  24558  cncms  24582  cnfldcusp  24584  rrxmvallem  24631  ivthicc  24685  ovolfioo  24694  ovolficc  24695  ovolficcss  24696  ovollb2lem  24715  ovoliunlem2  24730  ovolshftlem1  24736  ovolicc2  24749  ismbl  24753  voliunlem2  24778  volsup  24783  ioorf  24800  ioorinv  24803  ioorcl  24804  uniiccdif  24805  uniioovol  24806  uniiccvol  24807  uniioombllem2  24810  uniioombllem4  24813  dyaddisj  24823  dyadmax  24825  dyadmbllem  24826  dyadmbl  24827  opnmbllem  24828  opnmblALT  24830  volsup2  24832  mbfdm  24853  mbfima  24857  mbfid  24862  ismbfd  24866  mbfres2  24872  mbfposr  24879  mbfimaopnlem  24882  mbflimsup  24893  0plef  24899  i1f1lem  24916  itg11  24918  itg1addlem4  24926  itg1addlem4OLD  24927  i1fpos  24934  itg1le  24941  itg1climres  24942  mbfi1fseqlem5  24947  mbfi1flimlem  24950  xrge0f  24959  itg2ge0  24963  itg2seq  24970  itg2i1fseqle  24982  itg2i1fseq2  24984  itg2addlem  24986  itg2gt0  24988  limciun  25121  dvres  25138  dvres3a  25141  cpnres  25164  dvfre  25178  dvmptres3  25183  dvlip2  25222  dvgt0lem2  25230  deg1fvi  25313  uc1pmon1p  25379  fta1g  25395  ig1peu  25399  ig1pdvds  25404  plyco0  25416  plypf1  25436  dgrlem  25453  dgrub  25458  dgrlb  25460  coemulc  25479  plyreres  25506  plydivlem3  25518  plydivlem4  25519  plydiveu  25521  plyremlem  25527  fta1lem  25530  fta1  25531  vieta1lem2  25534  plyexmo  25536  elaa  25539  elqaalem3  25544  aannenlem1  25551  pserulm  25644  psercnlem2  25646  psercnlem1  25647  psercn  25648  abelth  25663  reeff1o  25669  pilem1  25673  recosf1o  25754  resinf1o  25755  efif1olem3  25763  efif1olem4  25764  efifo  25766  eff1olem  25767  ellogrn  25778  logcn  25865  dvloglem  25866  logf1o2  25868  efopnlem1  25874  efopnlem2  25875  efopn  25876  logtayl  25878  cxpcn3lem  25963  cxpcn3  25964  resqrtcn  25965  asinneg  26099  areambl  26171  emcllem7  26214  lgamgulm2  26248  basellem4  26296  sqff1o  26394  dvdsmulf1o  26406  fsumdvdsmul  26407  ostthlem1  26838  ostth  26850  tglnfn  27006  f1otrg  27330  axlowdimlem6  27413  axlowdimlem8  27415  axlowdimlem9  27416  axlowdimlem11  27418  axlowdimlem12  27419  axlowdimlem17  27424  elntg2  27451  crctcshlem4  28283  clwlkclwwlklem2  28462  eucrct2eupth  28707  ex-fpar  28924  cnnvm  29142  sspmlem  29192  nvo00  29221  nmlno0lem  29253  phoeqi  29317  ubthlem1  29330  hhip  29637  hhssabloilem  29721  hhssnv  29724  hhsssh  29729  occllem  29763  shsel  29774  chscllem2  30098  df0op2  30212  hoeq  30220  hocofni  30227  hoaddfni  30230  hosubfni  30231  hon0  30253  ho01i  30288  hoeq1  30290  elnlfn  30388  nmlnop0iALT  30455  lnopco0i  30464  imaelshi  30518  nlelchi  30521  rnbra  30567  cnvbraval  30570  kbass5  30580  hmopidmchi  30611  hmopidmpji  30612  foresf1o  30948  fimarab  31078  fcomptf  31093  ofpreima  31100  resf1o  31163  maprnin  31164  fpwrelmapffslem  31165  hashgt1  31226  s3clhash  31320  gsumpart  31413  xrge0tsmsd  31415  tocyc01  31483  cyc3evpm  31515  cycpmgcl  31518  cycpmconjslem2  31520  cyc3conja  31522  kerunit  31616  dimval  31782  dimvalfi  31783  txomap  31880  locfinreflem  31886  hauseqcn  31944  xpinpreima  31952  xpinpreima2  31953  tpr2rico  31958  mndpluscn  31972  rmulccn  31974  raddcn  31975  xrge0pluscn  31986  xrge0tmdALT  31992  rge0scvg  31995  pl1cn  32001  elzrhunit  32025  qqhf  32032  cnrrext  32056  qqhre  32066  indpi1  32084  indpreima  32089  1stmbfm  32323  2ndmbfm  32324  mbfmcnt  32331  omssubadd  32363  carsggect  32381  eulerpartlemsv2  32421  eulerpartlems  32423  eulerpartlemv  32427  eulerpartlemb  32431  eulerpartlemf  32433  eulerpartlemt  32434  eulerpartlemmf  32438  eulerpartlemgvv  32439  eulerpartlemgh  32441  eulerpartlemgs2  32443  sseqmw  32454  sseqf  32455  sseqp1  32458  fiblem  32461  fibp1  32464  plymul02  32621  signsvtn0  32645  signstres  32650  signshlen  32665  reprinrn  32694  circlemethhgt  32719  txsconnlem  33298  iccllysconn  33308  rellysconn  33309  cvmseu  33334  cvmliftmolem2  33340  cvmliftlem6  33348  cvmliftlem7  33349  cvmliftlem8  33350  cvmliftlem9  33351  cvmliftlem11  33353  cvmliftlem15  33356  cvmlift2lem7  33367  cvmlift2lem10  33370  cvmlift3lem8  33384  cvmlift3lem9  33385  mvrsfpw  33564  mrsubff1  33572  msrid  33603  msrfo  33604  elmsta  33606  mtyf  33610  msubff1  33614  vhmcls  33624  mclsax  33627  elmthm  33634  mthmblem  33638  mclsppslem  33641  iprodefisumlem  33802  soseq  33897  noetasuplem4  33998  madeval2  34096  elold  34112  madeoldsuc  34126  fullfunfnv  34307  fullfunfv  34308  tailfb  34625  filnetlem4  34629  taupilem3  35548  icoreresf  35581  icoreelrnab  35583  relowlssretop  35592  relowlpssretop  35593  unccur  35818  matunitlindflem1  35831  matunitlindflem2  35832  ptrecube  35835  poimirlem28  35863  poimirlem32  35867  heicant  35870  opnmbllem0  35871  mblfinlem1  35872  mblfinlem2  35873  volsupnfl  35880  cnambfre  35883  dvtan  35885  itg2addnclem  35886  itg2addnclem2  35887  ftc1anclem3  35910  ftc1anclem5  35912  ftc1anclem7  35914  ftc1anclem8  35915  ftc1anc  35916  areacirc  35928  indexdom  35950  sdclem2  35958  sstotbnd2  35990  sstotbnd  35991  isbndx  35998  isbnd3b  36001  prdsbnd  36009  prdstotbnd  36010  ismtyhmeolem  36020  heibor1lem  36025  heiborlem1  36027  heibor  36037  rrnequiv  36051  keridl  36248  ellkr  37313  lkr0f  37318  cdleme50rnlem  38768  sticksstones11  40325  sticksstones19  40334  sticksstones22  40337  fsuppind  40487  elrfirn  40725  ismrcd2  40729  isnacs2  40736  nacsfix  40742  mapfzcons1  40747  mzpcompact2lem  40781  eq0rabdioph  40806  eldioph4b  40841  diophren  40843  pw2f1ocnv  41068  pw2f1o2val2  41071  lmhmfgsplit  41120  pwssplit4  41123  hbt  41164  mpaaeu  41184  mendring  41226  proot1mul  41233  proot1hash  41234  proot1ex  41235  deg1mhm  41241  fgraphopab  41244  hausgraph  41246  ofsubid  42168  expgrowthi  42177  expgrowth  42179  binomcxplemdvbinom  42197  binomcxplemcvg  42198  binomcxplemnotnn0  42200  rfcnpre1  42788  rfcnpre2  42800  cncmpmax  42801  rfcnpre3  42802  rfcnpre4  42803  elixpconstg  42865  ffi  42942  dffo3f  42950  islptre  43402  resincncf  43658  dvcosre  43695  dvresntr  43701  volioof  43770  stoweidlem48  43831  fourierdlem12  43902  fourierdlem15  43905  fourierdlem41  43931  fourierdlem42  43932  fourierdlem46  43935  fourierdlem48  43937  fourierdlem49  43938  fourierdlem54  43943  fourierdlem56  43945  fourierdlem62  43951  fourierdlem64  43953  fourierdlem65  43954  fourierdlem73  43962  fourierdlem74  43963  fourierdlem75  43964  fourierdlem102  43991  fourierdlem103  43992  fourierdlem104  43993  fourierdlem114  44003  sge0split  44190  elhoi  44323  mbfresmf  44520  cfsetsnfsetf1  44810  cfsetsnfsetfo  44811  focofob  44829  f1ocof1ob  44830  fafvelcdm  44919  ffnafv  44920  fafv2elcdm  44983  fafv2elrnb  44984  imarnf1pr  45031  2ffzoeq  45077  fundcmpsurbijinjpreimafv  45116  fundcmpsurinjimaid  45120  fargshiftfv  45148  fargshiftf  45149  fargshiftf1  45150  fargshiftfo  45151  zrinitorngc  45815  zrtermorngc  45816  zrtermoringc  45885  fdmdifeqresdif  45934  fdivmpt  46143  fdivmptf  46144  refdivmptf  46145  1arymaptf1  46245  2arymaptf1  46256  ackfnnn0  46288  aacllem  46762