Theorem ffn 6707

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

This proof depends on syntax axioms:   → wi 4   ⊆ wss 3899  ran crn 5652   Fn wfn 6532  ⟶wf 6533

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 6541

This theorem is used by:  ffnd  6708  ffun  6710  ffunOLD  6711  frel  6713  fdm  6717  ffrn  6721  fresin  6749  fresaun  6751  fresaunres2  6752  fcoi1  6754  feu  6756  f0bi  6763  dffo2  6798  fimadmfo  6803  fdmeu  6939  feqmptdf  6953  fimarab  6957  fvco3  6983  ffvelcdm  7079  dff2  7097  dffo3  7100  dffo4  7101  dffo5  7102  dffo3f  7104  f1ompt  7109  ffnfv  7117  fcdmssb  7120  fcompt  7132  fsn2  7135  fprb  7197  fconst2g  7207  fpr2g  7215  fex  7230  dff13  7256  nvocnv  7287  soisores  7333  fdmexb  7917  resf1extb  7944  fo1stres  8025  fo2ndres  8026  1stcof  8029  2ndcof  8030  curry1f  8115  curry2f  8117  fparlem1  8121  fparlem2  8122  fo2ndf  8130  soseq  8169  tposf2  8260  smo11  8365  fsetexb  8879  mapsnd  8907  pw2f1olem  9093  mapen  9153  mapunen  9158  fissuni  9339  fipreima  9340  indexfi  9342  mapfien  9393  oismo  9527  cantnflt  9666  cantnfp1lem3  9674  cantnflem4  9686  tcrank  9894  updjudhcoinlf  10006  updjudhcoinrg  10007  updjud  10008  infpwfien  10134  cardinfima  10169  dfacacn  10213  cfflb  10330  cofsmo  10340  cfcoflem  10343  coftr  10344  fin23lem40  10422  axdc3lem2  10522  ac6num  10550  ac6c4  10552  ac6s2  10557  ttukeylem6  10585  iunfo  10616  pwcfsdom  10661  fpwwe2lem5  10713  fpwwe2lem7  10715  pwfseqlem3  10738  inar1  10853  tskcard  10859  tskuni  10861  tskurn  10867  gruima  10880  nqerrel  11010  recmulnq  11042  dmrecnq  11046  axpre-sup  11247  ofsubeq0  12310  indpi1  12327  dfz2  12705  uzn0  12975  rpnnen1lem3  13100  rpnnen1lem5  13102  unirnioo  13573  dfioo2  13574  ioorebas  13575  fseq1p1m1  13725  2ffzeq  13776  fvinim0ffz  13917  injresinjlem  13918  fsequb2  14112  fseqsupcl  14113  fseqsupubi  14114  ser0f  14191  hashgval  14470  hashinf  14472  hashresfn  14477  ffz0hash  14585  fnfzo0hash  14588  wrdred1hash  14699  revlen  14904  revrev  14909  repswlen  14920  repsdf2  14922  cshword  14935  0csh0  14937  lenco  14976  s1co  14977  cshco  14980  swrdco  14981  s7f1o  15112  ofccat  15115  shftf  15225  uzin2  15505  rexanuz  15506  limsuple  15638  limsupval2  15640  rlimres  15718  lo1res  15719  rlimresb  15725  isercolllem2  15826  isercolllem3  15827  isercoll  15828  supcvg  16018  prodf1f  16054  eff2  16260  reeff1  16281  tanval  16289  ruclem4  16395  ruclem12  16402  prmreclem6  17092  1arithlem4  17097  1arith  17098  vdwmc  17149  vdwlem1  17152  vdwlem8  17159  vdwlem13  17164  ramval  17179  0ram  17191  0ram2  17192  0ramcl  17194  ramcl  17200  fsets  17340  firest  17596  0ssc  18005  0subcat  18006  isfull2  18081  arwhoma  18213  gsumval2a  18867  isgrpinv  19197  kerf1ghm  19454  f1omvdconj  19653  pmtrmvd  19663  pmtrfinv  19668  pmtrdifellem4  19686  efgsfo  19946  efgredlem  19954  efgcpbllemb  19962  frgpup3lem  19984  0frgp  19986  gexex  20060  torsubg  20061  gsumval3  20114  gsumzres  20116  gsummptmhm  20147  gsumzoppg  20151  dprdf1o  20241  dprd2db  20252  zrinitorngc  20887  zrtermorngc  20888  zrtermoringc  20920  srngf1o  21098  lmhmima  21315  lmhmpreima  21316  lmhmrnlss  21318  lspextmo  21324  pwssplit1  21327  cnfldadd  21677  cnfldmul  21679  cnfldplusf  21698  cnfldsub  21699  chrrhm  21830  znunit  21862  psgnevpmb  21886  psgndiflemB  21899  mpofrlmd  22076  frlmipval  22078  frlmphl  22080  frlmlbs  22096  frlmup4  22100  ellspd  22101  lindfmm  22126  lsslindf  22129  psrbaglefi  22227  psrlidm  22262  mplmonmul  22338  evlseu  22385  mpfconst  22411  mpfproj  22412  mpfsubrg  22413  coe1sclmulfv  22595  pf1const  22657  pf1id  22658  pf1subrg  22659  mpfpf1  22662  pf1mpf  22663  mamuass  22710  mamudi  22711  mamudir  22712  mamuvs1  22713  mamuvs2  22714  1mavmul  22856  mavmulass  22857  mdetunilem7  22926  madutpos  22950  matunitlindflem1  22987  matunitlindflem2  22988  lecldbas  23530  lmbr2  23570  cncnpi  23589  cncnp  23591  cnpdis  23604  lmff  23612  pnrmopn  23654  dnsconst  23689  cmpsub  23711  tgcmp  23712  hauscmplem  23717  2ndcctbss  23767  2ndcomap  23770  2ndcsep  23771  1stccnp  23774  kgenidm  23859  iskgen2  23860  1stckgen  23866  kgen2cn  23871  ptpjpre1  23883  pttop  23894  ptuni  23906  ptval2  23913  tx1cn  23921  tx2cn  23922  ptpjcn  23923  ptpjopn  23924  ptclsg  23927  ptcnplem  23933  upxp  23935  txcnmpt  23936  uptx  23937  txcmplem2  23954  txkgen  23964  xkoptsub  23966  xkopt  23967  xkococnlem  23971  xkococn  23972  ptcmpfi  24125  zfbas  24208  uzrest  24209  rnelfmlem  24264  rnelfm  24265  fmfnfmlem2  24267  fmfnfm  24270  lmflf  24317  alexsubALT  24363  clssubg  24421  qustgplem  24433  tsmsres  24456  tsmsxplem1  24465  ucncn  24596  xmettpos  24661  imasdsf1olem  24685  blrnps  24720  blrn  24721  xmeterval  24744  tmslem  24794  tmsxms  24798  imasf1oxms  24801  prdsxms  24842  blval2  24874  metuel2  24877  isngp2  24909  isngp3  24910  tngngp2  24964  isnghm  25035  qtopbaslem  25070  qdensere  25081  cnbl0  25085  cnblcld  25086  cnfldms  25087  blssioo  25107  tgioo  25108  tgqioo  25112  xrtgioo  25119  xrsdsre  25123  xrge0tsms  25147  bndth  25272  lebnumlem3  25277  nmhmcn  25434  cphsqrtcl  25498  lmmbr2  25573  caucfil  25597  causs  25612  lmcau  25627  bcth3  25645  cncms  25669  cnfldcusp  25671  rrxmvallem  25718  ivthicc  25772  ovolfioo  25781  ovolficc  25782  ovolficcss  25783  ovollb2lem  25802  ovoliunlem2  25817  ovolshftlem1  25823  ovolicc2  25836  ismbl  25840  voliunlem2  25865  volsup  25870  ioorf  25887  ioorinv  25890  ioorcl  25891  uniiccdif  25892  uniioovol  25893  uniiccvol  25894  uniioombllem2  25897  uniioombllem4  25900  dyaddisj  25910  dyadmax  25912  dyadmbllem  25913  dyadmbl  25914  opnmbllem  25915  opnmblALT  25917  volsup2  25919  mbfdm  25940  mbfima  25944  mbfid  25949  ismbfd  25953  mbfres2  25959  mbfposr  25966  mbfimaopnlem  25969  mbflimsup  25980  0plef  25986  i1f1lem  26003  itg11  26005  itg1addlem4  26013  i1fpos  26020  itg1le  26027  itg1climres  26028  mbfi1fseqlem5  26033  mbfi1flimlem  26036  xrge0f  26045  itg2ge0  26049  itg2seq  26056  itg2i1fseqle  26068  itg2i1fseq2  26070  itg2addlem  26072  itg2gt0  26074  limciun  26207  dvres  26224  dvres3a  26227  cpnres  26250  dvfre  26264  dvmptres3  26269  dvlip2  26308  dvgt0lem2  26316  deg1fvi  26396  uc1pmon1p  26463  fta1g  26481  ig1peu  26486  ig1pdvds  26491  plyco0  26503  plypf1  26524  dgrlem  26541  dgrub  26546  dgrlb  26548  coemulc  26567  plymul02  26594  plyreres  26597  plydivlem3  26609  plydivlem4  26610  plydiveu  26612  plyremlem  26618  fta1lem  26621  fta1  26622  vieta1lem2  26627  plyexmo  26629  elaa  26632  elqaalem3  26637  aannenlem1  26648  pserulm  26742  psercnlem2  26744  psercnlem1  26745  psercn  26746  abelth  26761  reeff1o  26767  pilem1  26771  recosf1o  26856  resinf1o  26857  efif1olem3  26865  efif1olem4  26866  efifo  26868  eff1olem  26869  ellogrn  26880  logcn  26968  dvloglem  26969  logf1o2  26971  efopnlem1  26977  efopnlem2  26978  efopn  26979  logtayl  26981  cxpcn3lem  27068  cxpcn3  27069  resqrtcn  27070  asinneg  27207  areambl  27279  emcllem7  27322  lgamgulm2  27356  basellem4  27404  sqff1o  27502  mpodvdsmulf1o  27514  fsumdvdsmul  27515  dvdsmulf1o  27516  ostthlem1  27947  ostth  27959  noetasuplem4  28086  madeval2  28212  elold  28238  old1  28244  madeoldsuc  28264  tglnfn  29003  tgplnfn  29246  f1otrg  29441  axlowdimlem6  29518  axlowdimlem8  29520  axlowdimlem9  29521  axlowdimlem11  29523  axlowdimlem12  29524  axlowdimlem17  29529  elntg2  29556  dfpth2  30307  cyclnumvtx  30381  crctcshlem4  30402  clwlkclwwlklem2  30584  eucrct2eupth  30839  ex-fpar  31056  cnnvm  31277  sspmlem  31327  nvo00  31356  nmlno0lem  31388  phoeqi  31452  ubthlem1  31465  hhip  31772  hhssabloilem  31856  hhssnv  31859  hhsssh  31864  occllem  31898  shsel  31909  chscllem2  32233  df0op2  32347  hoeq  32355  hocofni  32362  hoaddfni  32365  hosubfni  32366  hon0  32388  ho01i  32423  hoeq1  32425  elnlfn  32523  nmlnop0iALT  32590  lnopco0i  32599  imaelshi  32653  nlelchi  32656  rnbra  32702  cnvbraval  32705  kbass5  32715  hmopidmchi  32746  hmopidmpji  32747  foresf1o  33093  fcomptf  33245  ofpreima  33252  resf1o  33315  maprnin  33316  fpwrelmapffslem  33317  hashgt1  33393  indpreima  33425  s3clhash  33505  gsumpart  33617  xrge0tsmsd  33627  tocyc01  33672  cyc3evpm  33704  cycpmgcl  33707  cycpmconjslem2  33709  cyc3conja  33711  kerunit  33879  1arithidomlem1  34060  1arithidomlem2  34061  1arithidom  34062  psrmonmul  34175  dimval  34226  dimvalfi  34227  ply1degltdimlem  34247  ply1degltdim  34248  elirng  34311  txomap  34459  locfinreflem  34465  hauseqcn  34523  xpinpreima  34531  xpinpreima2  34532  tpr2rico  34537  mndpluscn  34551  raddcn  34554  xrge0pluscn  34565  xrge0tmdALT  34571  rge0scvg  34574  pl1cn  34580  elzrhunit  34602  qqhf  34611  cnrrext  34635  qqhre  34645  1stmbfm  34885  2ndmbfm  34886  mbfmcnt  34893  omssubadd  34925  carsggect  34943  eulerpartlemsv2  34983  eulerpartlems  34985  eulerpartlemv  34989  eulerpartlemb  34993  eulerpartlemf  34995  eulerpartlemt  34996  eulerpartlemmf  35000  eulerpartlemgvv  35001  eulerpartlemgh  35003  eulerpartlemgs2  35005  sseqmw  35016  sseqf  35017  sseqp1  35020  fiblem  35023  fibp1  35026  signsvtn0  35192  signstres  35197  signshlen  35212  reprinrn  35240  circlemethhgt  35265  txsconnlem  35984  iccllysconn  35994  rellysconn  35995  cvmseu  36020  cvmliftmolem2  36026  cvmliftlem6  36034  cvmliftlem7  36035  cvmliftlem8  36036  cvmliftlem9  36037  cvmliftlem11  36039  cvmliftlem15  36042  cvmlift2lem7  36053  cvmlift2lem10  36056  cvmlift3lem8  36070  cvmlift3lem9  36071  mvrsfpw  36250  mrsubff1  36258  msrid  36289  msrfo  36290  elmsta  36292  mtyf  36296  msubff1  36300  vhmcls  36310  mclsax  36313  elmthm  36320  mthmblem  36324  mclsppslem  36327  iprodefisumlem  36484  fullfunfnv  36690  fullfunfv  36691  tailfb  37145  filnetlem4  37149  regsfromunir1  37308  taupilem3  38220  icoreresf  38255  icoreelrnab  38257  relowlssretop  38266  relowlpssretop  38267  unccur  38506  ptrecube  38518  poimirlem28  38546  poimirlem32  38550  heicant  38553  opnmbllem0  38554  mblfinlem1  38555  mblfinlem2  38556  volsupnfl  38563  cnambfre  38566  dvtan  38568  itg2addnclem  38569  itg2addnclem2  38570  ftc1anclem3  38593  ftc1anclem5  38595  ftc1anclem7  38597  ftc1anclem8  38598  ftc1anc  38599  areacirc  38611  indexdom  38648  sdclem2  38656  sstotbnd2  38688  sstotbnd  38689  isbndx  38696  isbnd3b  38699  prdsbnd  38707  prdstotbnd  38708  ismtyhmeolem  38718  heibor1lem  38723  heiborlem1  38725  heibor  38735  rrnequiv  38749  keridl  38946  ellkr  40126  lkr0f  40131  cdleme50rnlem  41581  aks6d1c2lem4  43157  aks6d1c5  43169  sticksstones11  43186  sticksstones19  43195  sticksstones22  43198  aks6d1c6lem4  43203  aks6d1c6isolem2  43205  fsuppind  43598  elrfirn  43685  ismrcd2  43689  isnacs2  43696  nacsfix  43702  mapfzcons1  43707  mzpcompact2lem  43741  eq0rabdioph  43766  eldioph4b  43797  diophren  43799  pw2f1ocnv  44023  pw2f1o2val2  44026  lmhmfgsplit  44072  pwssplit4  44075  hbt  44116  mpaaeu  44136  mendring  44174  proot1mul  44180  proot1hash  44181  proot1ex  44182  deg1mhm  44186  fgraphopab  44189  hausgraph  44191  nvocnvb  44407  ofsubid  45293  expgrowthi  45302  expgrowth  45304  binomcxplemdvbinom  45322  binomcxplemcvg  45323  binomcxplemnotnn0  45325  relpfrlem  45921  rfcnpre1  46005  rfcnpre2  46017  cncmpmax  46018  rfcnpre3  46019  rfcnpre4  46020  elixpconstg  46073  ffi  46157  islptre  46600  resincncf  46854  dvcosre  46891  dvresntr  46897  volioof  46966  stoweidlem48  47027  fourierdlem12  47098  fourierdlem15  47101  fourierdlem41  47127  fourierdlem42  47128  fourierdlem46  47131  fourierdlem54  47139  fourierdlem56  47141  fourierdlem62  47147  fourierdlem64  47149  fourierdlem65  47150  fourierdlem73  47158  fourierdlem74  47159  fourierdlem75  47160  fourierdlem102  47187  fourierdlem103  47188  fourierdlem104  47189  fourierdlem114  47199  sge0split  47388  elhoi  47521  mbfresmf  47718  cjnpoly  47908  cfsetsnfsetf1  48098  cfsetsnfsetfo  48099  focofob  48119  f1ocof1ob  48120  fafvelcdm  48209  ffnafv  48210  fafv2elcdm  48273  fafv2elrnb  48274  imarnf1pr  48321  2ffzoeq  48367  fundcmpsurbijinjpreimafv  48458  fundcmpsurinjimaid  48462  fargshiftfv  48490  fargshiftf  48491  fargshiftf1  48492  fargshiftfo  48493  cycl3grtri  49014  fdmdifeqresdif  49423  fdivmpt  49621  fdivmptf  49622  refdivmptf  49623  1arymaptf1  49723  2arymaptf1  49734  ackfnnn0  49766  homf0  50086  aacllem  50908