Theorem ffn 6702

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

This proof depends on syntax axioms:   → wi 4   ⊆ wss 3899  ran crn 5656   Fn wfn 6528  ⟶wf 6529

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 6537

This theorem is used by:  ffnd  6703  ffun  6705  ffunOLD  6706  frel  6708  fdm  6712  ffrn  6716  fresin  6744  fresaun  6746  fresaunres2  6747  fcoi1  6749  feu  6751  f0bi  6758  dffo2  6793  fimadmfo  6798  fdmeu  6934  feqmptdf  6948  fimarab  6952  fvco3  6978  ffvelcdm  7074  dff2  7092  dffo3  7095  dffo4  7096  dffo5  7097  dffo3f  7099  f1ompt  7104  ffnfv  7112  fcdmssb  7115  fcompt  7127  fsn2  7130  fprb  7192  fconst2g  7202  fpr2g  7210  fex  7225  dff13  7251  nvocnv  7282  soisores  7328  fdmexb  7904  resf1extb  7931  fo1stres  8012  fo2ndres  8013  1stcof  8016  2ndcof  8017  curry1f  8103  curry2f  8105  fparlem1  8109  fparlem2  8110  fo2ndf  8118  soseq  8157  tposf2  8248  smo11  8353  fsetexb  8865  mapsnd  8893  pw2f1olem  9079  mapen  9139  mapunen  9144  fissuni  9324  fipreima  9325  indexfi  9327  mapfien  9378  oismo  9512  cantnflt  9651  cantnfp1lem3  9659  cantnflem4  9671  tcrank  9866  updjudhcoinlf  9937  updjudhcoinrg  9938  updjud  9939  infpwfien  10065  cardinfima  10100  dfacacn  10144  cfflb  10261  cofsmo  10271  cfcoflem  10274  coftr  10275  fin23lem40  10353  axdc3lem2  10453  ac6num  10481  ac6c4  10483  ac6s2  10488  ttukeylem6  10516  iunfo  10547  pwcfsdom  10592  fpwwe2lem5  10644  fpwwe2lem7  10646  pwfseqlem3  10669  inar1  10784  tskcard  10790  tskuni  10792  tskurn  10798  gruima  10811  nqerrel  10941  recmulnq  10973  dmrecnq  10977  axpre-sup  11178  ofsubeq0  12239  indpi1  12256  dfz2  12634  uzn0  12904  rpnnen1lem3  13029  rpnnen1lem5  13031  unirnioo  13502  dfioo2  13503  ioorebas  13504  fseq1p1m1  13653  2ffzeq  13704  fvinim0ffz  13845  injresinjlem  13846  fsequb2  14040  fseqsupcl  14041  fseqsupubi  14042  ser0f  14119  hashgval  14397  hashinf  14399  hashresfn  14404  ffz0hash  14512  fnfzo0hash  14515  wrdred1hash  14626  revlen  14831  revrev  14836  repswlen  14847  repsdf2  14849  cshword  14862  0csh0  14864  lenco  14903  s1co  14904  cshco  14907  swrdco  14908  s7f1o  15039  ofccat  15042  shftf  15152  uzin2  15432  rexanuz  15433  limsuple  15565  limsupval2  15567  rlimres  15645  lo1res  15646  rlimresb  15652  isercolllem2  15753  isercolllem3  15754  isercoll  15755  supcvg  15945  prodf1f  15981  eff2  16187  reeff1  16208  tanval  16216  ruclem4  16322  ruclem12  16329  prmreclem6  17013  1arithlem4  17018  1arith  17019  vdwmc  17070  vdwlem1  17073  vdwlem8  17080  vdwlem13  17085  ramval  17100  0ram  17112  0ram2  17113  0ramcl  17115  ramcl  17121  fsets  17261  firest  17517  0ssc  17926  0subcat  17927  isfull2  18002  arwhoma  18134  gsumval2a  18787  isgrpinv  19117  kerf1ghm  19374  f1omvdconj  19573  pmtrmvd  19583  pmtrfinv  19588  pmtrdifellem4  19606  efgsfo  19866  efgredlem  19874  efgcpbllemb  19882  frgpup3lem  19904  0frgp  19906  gexex  19980  torsubg  19981  gsumval3  20034  gsumzres  20036  gsummptmhm  20067  gsumzoppg  20071  dprdf1o  20161  dprd2db  20172  zrinitorngc  20804  zrtermorngc  20805  zrtermoringc  20837  srngf1o  21014  lmhmima  21231  lmhmpreima  21232  lmhmrnlss  21234  lspextmo  21240  pwssplit1  21243  cnfldadd  21591  cnfldmul  21593  cnfldplusf  21612  cnfldsub  21613  chrrhm  21744  znunit  21776  psgnevpmb  21800  psgndiflemB  21813  mpofrlmd  21990  frlmipval  21992  frlmphl  21994  frlmlbs  22010  frlmup4  22014  ellspd  22015  lindfmm  22040  lsslindf  22043  psrbaglefi  22141  psrlidm  22176  mplmonmul  22252  evlseu  22299  mpfconst  22325  mpfproj  22326  mpfsubrg  22327  coe1sclmulfv  22509  pf1const  22571  pf1id  22572  pf1subrg  22573  mpfpf1  22576  pf1mpf  22577  mamuass  22624  mamudi  22625  mamudir  22626  mamuvs1  22627  mamuvs2  22628  1mavmul  22770  mavmulass  22771  mdetunilem7  22840  madutpos  22864  matunitlindflem1  22901  matunitlindflem2  22902  lecldbas  23444  lmbr2  23484  cncnpi  23503  cncnp  23505  cnpdis  23518  lmff  23526  pnrmopn  23568  dnsconst  23603  cmpsub  23625  tgcmp  23626  hauscmplem  23631  2ndcctbss  23681  2ndcomap  23684  2ndcsep  23685  1stccnp  23688  kgenidm  23773  iskgen2  23774  1stckgen  23780  kgen2cn  23785  ptpjpre1  23797  pttop  23808  ptuni  23820  ptval2  23827  tx1cn  23835  tx2cn  23836  ptpjcn  23837  ptpjopn  23838  ptclsg  23841  ptcnplem  23847  upxp  23849  txcnmpt  23850  uptx  23851  txcmplem2  23868  txkgen  23878  xkoptsub  23880  xkopt  23881  xkococnlem  23885  xkococn  23886  ptcmpfi  24039  zfbas  24122  uzrest  24123  rnelfmlem  24178  rnelfm  24179  fmfnfmlem2  24181  fmfnfm  24184  lmflf  24231  alexsubALT  24277  clssubg  24335  qustgplem  24347  tsmsres  24370  tsmsxplem1  24379  ucncn  24510  xmettpos  24575  imasdsf1olem  24599  blrnps  24634  blrn  24635  xmeterval  24658  tmslem  24708  tmsxms  24712  imasf1oxms  24715  prdsxms  24756  blval2  24788  metuel2  24791  isngp2  24823  isngp3  24824  tngngp2  24878  isnghm  24949  qtopbaslem  24984  qdensere  24995  cnbl0  24999  cnblcld  25000  cnfldms  25001  blssioo  25021  tgioo  25022  tgqioo  25026  xrtgioo  25033  xrsdsre  25037  xrge0tsms  25061  bndth  25186  lebnumlem3  25191  nmhmcn  25348  cphsqrtcl  25412  lmmbr2  25487  caucfil  25511  causs  25526  lmcau  25541  bcth3  25559  cncms  25583  cnfldcusp  25585  rrxmvallem  25632  ivthicc  25686  ovolfioo  25695  ovolficc  25696  ovolficcss  25697  ovollb2lem  25716  ovoliunlem2  25731  ovolshftlem1  25737  ovolicc2  25750  ismbl  25754  voliunlem2  25779  volsup  25784  ioorf  25801  ioorinv  25804  ioorcl  25805  uniiccdif  25806  uniioovol  25807  uniiccvol  25808  uniioombllem2  25811  uniioombllem4  25814  dyaddisj  25824  dyadmax  25826  dyadmbllem  25827  dyadmbl  25828  opnmbllem  25829  opnmblALT  25831  volsup2  25833  mbfdm  25854  mbfima  25858  mbfid  25863  ismbfd  25867  mbfres2  25873  mbfposr  25880  mbfimaopnlem  25883  mbflimsup  25894  0plef  25900  i1f1lem  25917  itg11  25919  itg1addlem4  25927  i1fpos  25934  itg1le  25941  itg1climres  25942  mbfi1fseqlem5  25947  mbfi1flimlem  25950  xrge0f  25959  itg2ge0  25963  itg2seq  25970  itg2i1fseqle  25982  itg2i1fseq2  25984  itg2addlem  25986  itg2gt0  25988  limciun  26121  dvres  26138  dvres3a  26141  cpnres  26164  dvfre  26178  dvmptres3  26183  dvlip2  26222  dvgt0lem2  26230  deg1fvi  26310  uc1pmon1p  26377  fta1g  26395  ig1peu  26400  ig1pdvds  26405  plyco0  26417  plypf1  26438  dgrlem  26455  dgrub  26460  dgrlb  26462  coemulc  26481  plymul02  26510  plyreres  26513  plydivlem3  26525  plydivlem4  26526  plydiveu  26528  plyremlem  26534  fta1lem  26537  fta1  26538  vieta1lem2  26543  plyexmo  26545  elaa  26548  elqaalem3  26553  aannenlem1  26564  pserulm  26658  psercnlem2  26660  psercnlem1  26661  psercn  26662  abelth  26677  reeff1o  26683  pilem1  26687  recosf1o  26772  resinf1o  26773  efif1olem3  26781  efif1olem4  26782  efifo  26784  eff1olem  26785  ellogrn  26796  logcn  26884  dvloglem  26885  logf1o2  26887  efopnlem1  26893  efopnlem2  26894  efopn  26895  logtayl  26897  cxpcn3lem  26984  cxpcn3  26985  resqrtcn  26986  asinneg  27123  areambl  27195  emcllem7  27238  lgamgulm2  27272  basellem4  27320  sqff1o  27418  mpodvdsmulf1o  27430  fsumdvdsmul  27431  dvdsmulf1o  27432  ostthlem1  27863  ostth  27875  noetasuplem4  27972  madeval2  28098  elold  28124  old1  28130  madeoldsuc  28150  tglnfn  28889  tgplnfn  29132  f1otrg  29327  axlowdimlem6  29404  axlowdimlem8  29406  axlowdimlem9  29407  axlowdimlem11  29409  axlowdimlem12  29410  axlowdimlem17  29415  elntg2  29442  dfpth2  30193  cyclnumvtx  30267  crctcshlem4  30288  clwlkclwwlklem2  30470  eucrct2eupth  30725  ex-fpar  30942  cnnvm  31163  sspmlem  31213  nvo00  31242  nmlno0lem  31274  phoeqi  31338  ubthlem1  31351  hhip  31658  hhssabloilem  31742  hhssnv  31745  hhsssh  31750  occllem  31784  shsel  31795  chscllem2  32119  df0op2  32233  hoeq  32241  hocofni  32248  hoaddfni  32251  hosubfni  32252  hon0  32274  ho01i  32309  hoeq1  32311  elnlfn  32409  nmlnop0iALT  32476  lnopco0i  32485  imaelshi  32539  nlelchi  32542  rnbra  32588  cnvbraval  32591  kbass5  32601  hmopidmchi  32632  hmopidmpji  32633  foresf1o  32979  fcomptf  33131  ofpreima  33138  resf1o  33201  maprnin  33202  fpwrelmapffslem  33203  hashgt1  33279  indpreima  33311  s3clhash  33391  gsumpart  33503  xrge0tsmsd  33513  tocyc01  33558  cyc3evpm  33590  cycpmgcl  33593  cycpmconjslem2  33595  cyc3conja  33597  kerunit  33765  1arithidomlem1  33945  1arithidomlem2  33946  1arithidom  33947  psrmonmul  34060  dimval  34111  dimvalfi  34112  ply1degltdimlem  34132  ply1degltdim  34133  elirng  34196  txomap  34344  locfinreflem  34350  hauseqcn  34408  xpinpreima  34416  xpinpreima2  34417  tpr2rico  34422  mndpluscn  34436  raddcn  34439  xrge0pluscn  34450  xrge0tmdALT  34456  rge0scvg  34459  pl1cn  34465  elzrhunit  34487  qqhf  34496  cnrrext  34520  qqhre  34530  1stmbfm  34771  2ndmbfm  34772  mbfmcnt  34779  omssubadd  34811  carsggect  34829  eulerpartlemsv2  34869  eulerpartlems  34871  eulerpartlemv  34875  eulerpartlemb  34879  eulerpartlemf  34881  eulerpartlemt  34882  eulerpartlemmf  34886  eulerpartlemgvv  34887  eulerpartlemgh  34889  eulerpartlemgs2  34891  sseqmw  34902  sseqf  34903  sseqp1  34906  fiblem  34909  fibp1  34912  signsvtn0  35078  signstres  35083  signshlen  35098  reprinrn  35126  circlemethhgt  35151  txsconnlem  35819  iccllysconn  35829  rellysconn  35830  cvmseu  35855  cvmliftmolem2  35861  cvmliftlem6  35869  cvmliftlem7  35870  cvmliftlem8  35871  cvmliftlem9  35872  cvmliftlem11  35874  cvmliftlem15  35877  cvmlift2lem7  35888  cvmlift2lem10  35891  cvmlift3lem8  35905  cvmlift3lem9  35906  mvrsfpw  36085  mrsubff1  36093  msrid  36124  msrfo  36125  elmsta  36127  mtyf  36131  msubff1  36135  vhmcls  36145  mclsax  36148  elmthm  36155  mthmblem  36159  mclsppslem  36162  iprodefisumlem  36319  fullfunfnv  36525  fullfunfv  36526  tailfb  36996  filnetlem4  37000  regsfromunir1  37159  taupilem3  38071  icoreresf  38106  icoreelrnab  38108  relowlssretop  38117  relowlpssretop  38118  unccur  38357  ptrecube  38369  poimirlem28  38397  poimirlem32  38401  heicant  38404  opnmbllem0  38405  mblfinlem1  38406  mblfinlem2  38407  volsupnfl  38414  cnambfre  38417  dvtan  38419  itg2addnclem  38420  itg2addnclem2  38421  ftc1anclem3  38444  ftc1anclem5  38446  ftc1anclem7  38448  ftc1anclem8  38449  ftc1anc  38450  areacirc  38462  indexdom  38484  sdclem2  38492  sstotbnd2  38524  sstotbnd  38525  isbndx  38532  isbnd3b  38535  prdsbnd  38543  prdstotbnd  38544  ismtyhmeolem  38554  heibor1lem  38559  heiborlem1  38561  heibor  38571  rrnequiv  38585  keridl  38782  ellkr  39962  lkr0f  39967  cdleme50rnlem  41417  aks6d1c2lem4  42993  aks6d1c5  43005  sticksstones11  43022  sticksstones19  43031  sticksstones22  43034  aks6d1c6lem4  43039  aks6d1c6isolem2  43041  fsuppind  43436  elrfirn  43540  ismrcd2  43544  isnacs2  43551  nacsfix  43557  mapfzcons1  43562  mzpcompact2lem  43596  eq0rabdioph  43621  eldioph4b  43652  diophren  43654  pw2f1ocnv  43878  pw2f1o2val2  43881  lmhmfgsplit  43927  pwssplit4  43930  hbt  43971  mpaaeu  43991  mendring  44029  proot1mul  44035  proot1hash  44036  proot1ex  44037  deg1mhm  44041  fgraphopab  44044  hausgraph  44046  nvocnvb  44262  ofsubid  45148  expgrowthi  45157  expgrowth  45159  binomcxplemdvbinom  45177  binomcxplemcvg  45178  binomcxplemnotnn0  45180  relpfrlem  45776  rfcnpre1  45853  rfcnpre2  45865  cncmpmax  45866  rfcnpre3  45867  rfcnpre4  45868  elixpconstg  45921  ffi  46005  islptre  46449  resincncf  46703  dvcosre  46740  dvresntr  46746  volioof  46815  stoweidlem48  46876  fourierdlem12  46947  fourierdlem15  46950  fourierdlem41  46976  fourierdlem42  46977  fourierdlem46  46980  fourierdlem54  46988  fourierdlem56  46990  fourierdlem62  46996  fourierdlem64  46998  fourierdlem65  46999  fourierdlem73  47007  fourierdlem74  47008  fourierdlem75  47009  fourierdlem102  47036  fourierdlem103  47037  fourierdlem104  47038  fourierdlem114  47048  sge0split  47237  elhoi  47370  mbfresmf  47567  cjnpoly  47757  cfsetsnfsetf1  47947  cfsetsnfsetfo  47948  focofob  47968  f1ocof1ob  47969  fafvelcdm  48058  ffnafv  48059  fafv2elcdm  48122  fafv2elrnb  48123  imarnf1pr  48170  2ffzoeq  48216  fundcmpsurbijinjpreimafv  48307  fundcmpsurinjimaid  48311  fargshiftfv  48339  fargshiftf  48340  fargshiftf1  48341  fargshiftfo  48342  cycl3grtri  48863  fdmdifeqresdif  49272  fdivmpt  49470  fdivmptf  49471  refdivmptf  49472  1arymaptf1  49572  2arymaptf1  49583  ackfnnn0  49615  homf0  49935  aacllem  50772