Theorem ffn 6712

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

This proof depends on syntax axioms:   → wi 4   ⊆ wss 3896  ran crn 5651   Fn wfn 6536  ⟶wf 6537

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-f 6545

This theorem is used by:  ffnd  6713  ffun  6715  ffunOLD  6716  frel  6718  fdm  6722  ffrn  6726  fresin  6754  fresaun  6756  fresaunres2  6757  fcoi1  6759  feu  6761  f0bi  6768  dffo2  6803  fimadmfo  6808  fdmeu  6944  feqmptdf  6958  fimarab  6962  fvco3  6988  ffvelcdm  7084  dff2  7102  dffo3  7105  dffo4  7106  dffo5  7107  dffo3f  7109  f1ompt  7114  ffnfv  7122  fcdmssb  7125  fcompt  7137  fsn2  7140  fprb  7201  fconst2g  7211  fpr2g  7219  fex  7234  dff13  7260  nvocnv  7291  soisores  7337  fdmexb  7921  resf1extb  7948  fo1stres  8029  fo2ndres  8030  1stcof  8033  2ndcof  8034  curry1f  8121  curry2f  8123  fparlem1  8127  fparlem2  8128  fo2ndf  8136  soseq  8180  tposf2  8272  smo11  8377  fsetexb  8891  mapsnd  8919  pw2f1olem  9105  mapen  9165  mapunen  9170  fissuni  9351  fipreima  9352  indexfi  9354  mapfien  9405  oismo  9539  cantnflt  9678  cantnfp1lem3  9686  cantnflem4  9698  tcrank  9906  updjudhcoinlf  10018  updjudhcoinrg  10019  updjud  10020  infpwfien  10146  cardinfima  10181  dfacacn  10225  cfflb  10342  cofsmo  10352  cfcoflem  10355  coftr  10356  fin23lem40  10434  axdc3lem2  10534  ac6num  10562  ac6c4  10564  ac6s2  10569  ttukeylem6  10597  iunfo  10628  pwcfsdom  10673  fpwwe2lem5  10725  fpwwe2lem7  10727  pwfseqlem3  10750  inar1  10865  tskcard  10871  tskuni  10873  tskurn  10879  gruima  10892  nqerrel  11022  recmulnq  11054  dmrecnq  11058  axpre-sup  11259  ofsubeq0  12322  indpi1  12339  dfz2  12717  uzn0  12987  rpnnen1lem3  13112  rpnnen1lem5  13114  unirnioo  13585  dfioo2  13586  ioorebas  13587  fseq1p1m1  13737  2ffzeq  13788  fvinim0ffz  13929  injresinjlem  13930  fsequb2  14124  fseqsupcl  14125  fseqsupubi  14126  ser0f  14203  hashgval  14482  hashinf  14484  hashresfn  14489  ffz0hash  14597  fnfzo0hash  14600  wrdred1hash  14711  revlen  14917  revrev  14922  repswlen  14933  repsdf2  14935  cshword  14948  0csh0  14950  lenco  14989  s1co  14990  cshco  14993  swrdco  14994  s7f1o  15126  ofccat  15129  shftf  15239  uzin2  15519  rexanuz  15520  limsuple  15652  limsupval2  15654  rlimres  15732  lo1res  15733  rlimresb  15739  isercolllem2  15840  isercolllem3  15841  isercoll  15842  supcvg  16032  prodf1f  16068  eff2  16274  reeff1  16295  tanval  16303  ruclem4  16409  ruclem12  16416  prmreclem6  17106  1arithlem4  17111  1arith  17112  vdwmc  17163  vdwlem1  17166  vdwlem8  17173  vdwlem13  17178  ramval  17193  0ram  17205  0ram2  17206  0ramcl  17208  ramcl  17214  fsets  17354  firest  17610  0ssc  18019  0subcat  18020  isfull2  18095  arwhoma  18227  gsumval2a  18881  isgrpinv  19211  kerf1ghm  19468  f1omvdconj  19667  pmtrmvd  19677  pmtrfinv  19682  pmtrdifellem4  19700  efgsfo  19960  efgredlem  19968  efgcpbllemb  19976  frgpup3lem  19998  0frgp  20000  gexex  20074  torsubg  20075  gsumval3  20128  gsumzres  20130  gsummptmhm  20161  gsumzoppg  20165  dprdf1o  20255  dprd2db  20266  zrinitorngc  20901  zrtermorngc  20902  zrtermoringc  20934  srngf1o  21112  lmhmima  21329  lmhmpreima  21330  lmhmrnlss  21332  lspextmo  21338  pwssplit1  21341  cnfldadd  21691  cnfldmul  21693  cnfldplusf  21712  cnfldsub  21713  chrrhm  21844  znunit  21876  psgnevpmb  21900  psgndiflemB  21913  mpofrlmd  22090  frlmipval  22092  frlmphl  22094  frlmlbs  22110  frlmup4  22114  ellspd  22115  lindfmm  22140  lsslindf  22143  psrbaglefi  22241  psrlidm  22276  mplmonmul  22352  evlseu  22399  mpfconst  22425  mpfproj  22426  mpfsubrg  22427  coe1sclmulfv  22609  pf1const  22671  pf1id  22672  pf1subrg  22673  mpfpf1  22676  pf1mpf  22677  mamuass  22724  mamudi  22725  mamudir  22726  mamuvs1  22727  mamuvs2  22728  1mavmul  22870  mavmulass  22871  mdetunilem7  22940  madutpos  22964  matunitlindflem1  23001  matunitlindflem2  23002  lecldbas  23544  lmbr2  23584  cncnpi  23603  cncnp  23605  cnpdis  23618  lmff  23626  pnrmopn  23668  dnsconst  23703  cmpsub  23725  tgcmp  23726  hauscmplem  23731  2ndcctbss  23781  2ndcomap  23784  2ndcsep  23785  1stccnp  23788  kgenidm  23873  iskgen2  23874  1stckgen  23880  kgen2cn  23885  ptpjpre1  23897  pttop  23908  ptuni  23920  ptval2  23927  tx1cn  23935  tx2cn  23936  ptpjcn  23937  ptpjopn  23938  ptclsg  23941  ptcnplem  23947  upxp  23949  txcnmpt  23950  uptx  23951  txcmplem2  23968  txkgen  23978  xkoptsub  23980  xkopt  23981  xkococnlem  23985  xkococn  23986  ptcmpfi  24139  zfbas  24222  uzrest  24223  rnelfmlem  24278  rnelfm  24279  fmfnfmlem2  24281  fmfnfm  24284  lmflf  24331  alexsubALT  24377  clssubg  24435  qustgplem  24447  tsmsres  24470  tsmsxplem1  24479  ucncn  24610  xmettpos  24675  imasdsf1olem  24699  blrnps  24734  blrn  24735  xmeterval  24758  tmslem  24808  tmsxms  24812  imasf1oxms  24815  prdsxms  24856  blval2  24888  metuel2  24891  isngp2  24923  isngp3  24924  tngngp2  24978  isnghm  25049  qtopbaslem  25084  qdensere  25095  cnbl0  25099  cnblcld  25100  cnfldms  25101  blssioo  25121  tgioo  25122  tgqioo  25126  xrtgioo  25133  xrsdsre  25137  xrge0tsms  25161  bndth  25286  lebnumlem3  25291  nmhmcn  25448  cphsqrtcl  25512  lmmbr2  25587  caucfil  25611  causs  25626  lmcau  25641  bcth3  25659  cncms  25683  cnfldcusp  25685  rrxmvallem  25732  ivthicc  25786  ovolfioo  25795  ovolficc  25796  ovolficcss  25797  ovollb2lem  25816  ovoliunlem2  25831  ovolshftlem1  25837  ovolicc2  25850  ismbl  25854  voliunlem2  25879  volsup  25884  ioorf  25901  ioorinv  25904  ioorcl  25905  uniiccdif  25906  uniioovol  25907  uniiccvol  25908  uniioombllem2  25911  uniioombllem4  25914  dyaddisj  25924  dyadmax  25926  dyadmbllem  25927  dyadmbl  25928  opnmbllem  25929  opnmblALT  25931  volsup2  25933  mbfdm  25954  mbfima  25958  mbfid  25963  ismbfd  25967  mbfres2  25973  mbfposr  25980  mbfimaopnlem  25983  mbflimsup  25994  0plef  26000  i1f1lem  26017  itg11  26019  itg1addlem4  26027  i1fpos  26034  itg1le  26041  itg1climres  26042  mbfi1fseqlem5  26047  mbfi1flimlem  26050  xrge0f  26059  itg2ge0  26063  itg2seq  26070  itg2i1fseqle  26082  itg2i1fseq2  26084  itg2addlem  26086  itg2gt0  26088  limciun  26221  dvres  26238  dvres3a  26241  cpnres  26264  dvfre  26278  dvmptres3  26283  dvlip2  26322  dvgt0lem2  26330  deg1fvi  26410  uc1pmon1p  26477  fta1g  26495  ig1peu  26500  ig1pdvds  26505  plyco0  26517  plypf1  26538  dgrlem  26555  dgrub  26560  dgrlb  26562  coemulc  26581  plymul02  26608  plyreres  26611  plydivlem3  26623  plydivlem4  26624  plydiveu  26626  plyremlem  26632  fta1lem  26635  fta1  26636  vieta1lem2  26641  plyexmo  26643  elaa  26646  elqaalem3  26651  aannenlem1  26662  pserulm  26756  psercnlem2  26758  psercnlem1  26759  psercn  26760  abelth  26775  reeff1o  26781  pilem1  26785  recosf1o  26870  resinf1o  26871  efif1olem3  26879  efif1olem4  26880  efifo  26882  eff1olem  26883  ellogrn  26894  logcn  26982  dvloglem  26983  logf1o2  26985  efopnlem1  26991  efopnlem2  26992  efopn  26993  logtayl  26995  cxpcn3lem  27082  cxpcn3  27083  resqrtcn  27084  asinneg  27221  areambl  27293  emcllem7  27336  lgamgulm2  27370  basellem4  27418  sqff1o  27516  mpodvdsmulf1o  27528  fsumdvdsmul  27529  dvdsmulf1o  27530  ostthlem1  27961  ostth  27973  noetasuplem4  28100  madeval2  28226  elold  28252  old1  28258  madeoldsuc  28278  tglnfn  29017  tgplnfn  29260  f1otrg  29455  axlowdimlem6  29532  axlowdimlem8  29534  axlowdimlem9  29535  axlowdimlem11  29537  axlowdimlem12  29538  axlowdimlem17  29543  elntg2  29570  dfpth2  30321  cyclnumvtx  30395  crctcshlem4  30416  clwlkclwwlklem2  30598  eucrct2eupth  30853  ex-fpar  31070  cnnvm  31291  sspmlem  31341  nvo00  31370  nmlno0lem  31402  phoeqi  31466  ubthlem1  31479  hhip  31786  hhssabloilem  31870  hhssnv  31873  hhsssh  31878  occllem  31912  shsel  31923  chscllem2  32247  df0op2  32361  hoeq  32369  hocofni  32376  hoaddfni  32379  hosubfni  32380  hon0  32402  ho01i  32437  hoeq1  32439  elnlfn  32537  nmlnop0iALT  32604  lnopco0i  32613  imaelshi  32667  nlelchi  32670  rnbra  32716  cnvbraval  32719  kbass5  32729  hmopidmchi  32760  hmopidmpji  32761  foresf1o  33149  fcomptf  33301  ofpreima  33308  resf1o  33370  maprnin  33371  fpwrelmapffslem  33372  hashgt1  33448  indpreima  33480  s3clhash  33560  gsumpart  33672  xrge0tsmsd  33682  tocyc01  33727  cyc3evpm  33759  cycpmgcl  33762  cycpmconjslem2  33764  cyc3conja  33766  kerunit  33934  1arithidomlem1  34115  1arithidomlem2  34116  1arithidom  34117  psrmonmul  34230  dimval  34281  dimvalfi  34282  ply1degltdimlem  34302  ply1degltdim  34303  elirng  34366  txomap  34514  locfinreflem  34520  hauseqcn  34578  xpinpreima  34586  xpinpreima2  34587  tpr2rico  34592  mndpluscn  34606  raddcn  34609  xrge0pluscn  34620  xrge0tmdALT  34626  rge0scvg  34629  pl1cn  34635  elzrhunit  34657  qqhf  34666  cnrrext  34690  qqhre  34700  1stmbfm  34940  2ndmbfm  34941  mbfmcnt  34948  omssubadd  34980  carsggect  34998  eulerpartlemsv2  35038  eulerpartlems  35040  eulerpartlemv  35044  eulerpartlemb  35048  eulerpartlemf  35050  eulerpartlemt  35051  eulerpartlemmf  35055  eulerpartlemgvv  35056  eulerpartlemgh  35058  eulerpartlemgs2  35060  sseqmw  35071  sseqf  35072  sseqp1  35075  fiblem  35078  fibp1  35081  signsvtn0  35247  signstres  35252  signshlen  35267  reprinrn  35295  circlemethhgt  35320  ptpconn  36086  txsconnlem  36093  iccllysconn  36103  rellysconn  36104  cvmseu  36129  cvmliftmolem2  36135  cvmliftlem6  36143  cvmliftlem7  36144  cvmliftlem8  36145  cvmliftlem9  36146  cvmliftlem11  36148  cvmliftlem15  36151  cvmlift2lem7  36162  cvmlift2lem10  36165  cvmlift3lem8  36179  cvmlift3lem9  36180  mvrsfpw  36359  mrsubff1  36367  msrid  36398  msrfo  36399  elmsta  36401  mtyf  36405  msubff1  36409  vhmcls  36419  mclsax  36422  elmthm  36429  mthmblem  36433  mclsppslem  36436  iprodefisumlem  36599  fullfunfnv  36804  fullfunfv  36805  tailfb  37259  filnetlem4  37263  regsfromunir1  37422  taupilem3  38347  icoreresf  38382  icoreelrnab  38384  relowlssretop  38393  relowlpssretop  38394  unccur  38633  ptrecube  38645  poimirlem28  38673  poimirlem32  38677  heicant  38680  opnmbllem0  38681  mblfinlem1  38682  mblfinlem2  38683  volsupnfl  38690  cnambfre  38693  dvtan  38695  itg2addnclem  38696  itg2addnclem2  38697  ftc1anclem3  38720  ftc1anclem5  38722  ftc1anclem7  38724  ftc1anclem8  38725  ftc1anc  38726  areacirc  38738  indexdom  38775  sdclem2  38783  sstotbnd2  38815  sstotbnd  38816  isbndx  38823  isbnd3b  38826  prdsbnd  38834  prdstotbnd  38835  ismtyhmeolem  38845  heibor1lem  38850  heiborlem1  38852  heibor  38862  rrnequiv  38876  keridl  39073  ellkr  40253  lkr0f  40258  cdleme50rnlem  41708  aks6d1c2lem4  43284  aks6d1c5  43296  sticksstones11  43313  sticksstones19  43322  sticksstones22  43325  aks6d1c6lem4  43330  aks6d1c6isolem2  43332  fsuppind  43725  elrfirn  43813  ismrcd2  43817  isnacs2  43824  nacsfix  43830  mapfzcons1  43835  mzpcompact2lem  43869  eq0rabdioph  43894  eldioph4b  43925  diophren  43927  pw2f1ocnv  44151  pw2f1o2val2  44154  lmhmfgsplit  44195  pwssplit4  44198  hbt  44239  mpaaeu  44259  mendring  44297  proot1mul  44303  proot1hash  44304  proot1ex  44305  deg1mhm  44309  fgraphopab  44312  hausgraph  44314  nvocnvb  44530  ofsubid  45415  expgrowthi  45424  expgrowth  45426  binomcxplemdvbinom  45444  binomcxplemcvg  45445  binomcxplemnotnn0  45447  relpfrlem  46050  rfcnpre1  46143  rfcnpre2  46155  cncmpmax  46156  rfcnpre3  46157  rfcnpre4  46158  elixpconstg  46211  ffi  46295  islptre  46738  resincncf  46992  dvcosre  47029  dvresntr  47035  volioof  47104  stoweidlem48  47165  fourierdlem12  47236  fourierdlem15  47239  fourierdlem41  47265  fourierdlem42  47266  fourierdlem46  47269  fourierdlem54  47277  fourierdlem56  47279  fourierdlem62  47285  fourierdlem64  47287  fourierdlem65  47288  fourierdlem73  47296  fourierdlem74  47297  fourierdlem75  47298  fourierdlem102  47325  fourierdlem103  47326  fourierdlem104  47327  fourierdlem114  47337  sge0split  47526  elhoi  47659  mbfresmf  47856  cjnpoly  48046  cfsetsnfsetf1  48236  cfsetsnfsetfo  48237  focofob  48257  f1ocof1ob  48258  fafvelcdm  48347  ffnafv  48348  fafv2elcdm  48411  fafv2elrnb  48412  imarnf1pr  48459  2ffzoeq  48505  fundcmpsurbijinjpreimafv  48596  fundcmpsurinjimaid  48600  fargshiftfv  48628  fargshiftf  48629  fargshiftf1  48630  fargshiftfo  48631  cycl3grtri  49152  fdmdifeqresdif  49561  fdivmpt  49759  fdivmptf  49760  refdivmptf  49761  1arymaptf1  49861  2arymaptf1  49872  ackfnnn0  49904  homf0  50230  aacllem  51121