Theorem ffn 6710

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

This proof depends on syntax axioms:   → wi 4   ⊆ wss 3914  ran crn 5652   Fn wfn 6534  ⟶wf 6535

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 6543

This theorem is used by:  ffnd  6711  ffun  6713  ffunOLD  6714  frel  6716  fdm  6720  ffrn  6724  fresin  6752  fresaun  6754  fresaunres2  6755  fcoi1  6757  feu  6759  f0bi  6766  dffo2  6801  fimadmfo  6806  fdmeu  6942  feqmptdf  6956  fimarab  6960  fvco3  6986  ffvelcdm  7082  dff2  7100  dffo3  7103  dffo4  7104  dffo5  7105  dffo3f  7107  f1ompt  7112  ffnfv  7120  fcdmssb  7123  fcompt  7135  fsn2  7138  fprb  7200  fconst2g  7210  fpr2g  7218  fex  7233  dff13  7259  nvocnv  7290  soisores  7336  fdmexb  7920  resf1extb  7947  fo1stres  8028  fo2ndres  8029  1stcof  8032  2ndcof  8033  curry1f  8118  curry2f  8120  fparlem1  8124  fparlem2  8125  fo2ndf  8133  soseq  8177  tposf2  8268  smo11  8373  fsetexb  8887  mapsnd  8915  pw2f1olem  9101  mapen  9161  mapunen  9166  fissuni  9347  fipreima  9348  indexfi  9350  mapfien  9401  oismo  9535  cantnflt  9674  cantnfp1lem3  9682  cantnflem4  9694  tcrank  9902  updjudhcoinlf  10014  updjudhcoinrg  10015  updjud  10016  infpwfien  10142  cardinfima  10177  dfacacn  10221  cfflb  10338  cofsmo  10348  cfcoflem  10351  coftr  10352  fin23lem40  10430  axdc3lem2  10530  ac6num  10558  ac6c4  10560  ac6s2  10565  ttukeylem6  10593  iunfo  10624  pwcfsdom  10669  fpwwe2lem5  10721  fpwwe2lem7  10723  pwfseqlem3  10746  inar1  10861  tskcard  10867  tskuni  10869  tskurn  10875  gruima  10888  nqerrel  11018  recmulnq  11050  dmrecnq  11054  axpre-sup  11255  ofsubeq0  12318  indpi1  12335  dfz2  12713  uzn0  12983  rpnnen1lem3  13108  rpnnen1lem5  13110  unirnioo  13581  dfioo2  13582  ioorebas  13583  fseq1p1m1  13733  2ffzeq  13784  fvinim0ffz  13925  injresinjlem  13926  fsequb2  14120  fseqsupcl  14121  fseqsupubi  14122  ser0f  14199  hashgval  14478  hashinf  14480  hashresfn  14485  ffz0hash  14593  fnfzo0hash  14596  wrdred1hash  14707  revlen  14912  revrev  14917  repswlen  14928  repsdf2  14930  cshword  14943  0csh0  14945  lenco  14984  s1co  14985  cshco  14988  swrdco  14989  s7f1o  15120  ofccat  15123  shftf  15233  uzin2  15513  rexanuz  15514  limsuple  15646  limsupval2  15648  rlimres  15726  lo1res  15727  rlimresb  15733  isercolllem2  15834  isercolllem3  15835  isercoll  15836  supcvg  16026  prodf1f  16062  eff2  16268  reeff1  16289  tanval  16297  ruclem4  16403  ruclem12  16410  prmreclem6  17100  1arithlem4  17105  1arith  17106  vdwmc  17157  vdwlem1  17160  vdwlem8  17167  vdwlem13  17172  ramval  17187  0ram  17199  0ram2  17200  0ramcl  17202  ramcl  17208  fsets  17348  firest  17604  0ssc  18013  0subcat  18014  isfull2  18089  arwhoma  18221  gsumval2a  18875  isgrpinv  19205  kerf1ghm  19462  f1omvdconj  19661  pmtrmvd  19671  pmtrfinv  19676  pmtrdifellem4  19694  efgsfo  19954  efgredlem  19962  efgcpbllemb  19970  frgpup3lem  19992  0frgp  19994  gexex  20068  torsubg  20069  gsumval3  20122  gsumzres  20124  gsummptmhm  20155  gsumzoppg  20159  dprdf1o  20249  dprd2db  20260  zrinitorngc  20895  zrtermorngc  20896  zrtermoringc  20928  srngf1o  21106  lmhmima  21323  lmhmpreima  21324  lmhmrnlss  21326  lspextmo  21332  pwssplit1  21335  cnfldadd  21685  cnfldmul  21687  cnfldplusf  21706  cnfldsub  21707  chrrhm  21838  znunit  21870  psgnevpmb  21894  psgndiflemB  21907  mpofrlmd  22084  frlmipval  22086  frlmphl  22088  frlmlbs  22104  frlmup4  22108  ellspd  22109  lindfmm  22134  lsslindf  22137  psrbaglefi  22235  psrlidm  22270  mplmonmul  22346  evlseu  22393  mpfconst  22419  mpfproj  22420  mpfsubrg  22421  coe1sclmulfv  22603  pf1const  22665  pf1id  22666  pf1subrg  22667  mpfpf1  22670  pf1mpf  22671  mamuass  22718  mamudi  22719  mamudir  22720  mamuvs1  22721  mamuvs2  22722  1mavmul  22864  mavmulass  22865  mdetunilem7  22934  madutpos  22958  matunitlindflem1  22995  matunitlindflem2  22996  lecldbas  23538  lmbr2  23578  cncnpi  23597  cncnp  23599  cnpdis  23612  lmff  23620  pnrmopn  23662  dnsconst  23697  cmpsub  23719  tgcmp  23720  hauscmplem  23725  2ndcctbss  23775  2ndcomap  23778  2ndcsep  23779  1stccnp  23782  kgenidm  23867  iskgen2  23868  1stckgen  23874  kgen2cn  23879  ptpjpre1  23891  pttop  23902  ptuni  23914  ptval2  23921  tx1cn  23929  tx2cn  23930  ptpjcn  23931  ptpjopn  23932  ptclsg  23935  ptcnplem  23941  upxp  23943  txcnmpt  23944  uptx  23945  txcmplem2  23962  txkgen  23972  xkoptsub  23974  xkopt  23975  xkococnlem  23979  xkococn  23980  ptcmpfi  24133  zfbas  24216  uzrest  24217  rnelfmlem  24272  rnelfm  24273  fmfnfmlem2  24275  fmfnfm  24278  lmflf  24325  alexsubALT  24371  clssubg  24429  qustgplem  24441  tsmsres  24464  tsmsxplem1  24473  ucncn  24604  xmettpos  24669  imasdsf1olem  24693  blrnps  24728  blrn  24729  xmeterval  24752  tmslem  24802  tmsxms  24806  imasf1oxms  24809  prdsxms  24850  blval2  24882  metuel2  24885  isngp2  24917  isngp3  24918  tngngp2  24972  isnghm  25043  qtopbaslem  25078  qdensere  25089  cnbl0  25093  cnblcld  25094  cnfldms  25095  blssioo  25115  tgioo  25116  tgqioo  25120  xrtgioo  25127  xrsdsre  25131  xrge0tsms  25155  bndth  25280  lebnumlem3  25285  nmhmcn  25442  cphsqrtcl  25506  lmmbr2  25581  caucfil  25605  causs  25620  lmcau  25635  bcth3  25653  cncms  25677  cnfldcusp  25679  rrxmvallem  25726  ivthicc  25780  ovolfioo  25789  ovolficc  25790  ovolficcss  25791  ovollb2lem  25810  ovoliunlem2  25825  ovolshftlem1  25831  ovolicc2  25844  ismbl  25848  voliunlem2  25873  volsup  25878  ioorf  25895  ioorinv  25898  ioorcl  25899  uniiccdif  25900  uniioovol  25901  uniiccvol  25902  uniioombllem2  25905  uniioombllem4  25908  dyaddisj  25918  dyadmax  25920  dyadmbllem  25921  dyadmbl  25922  opnmbllem  25923  opnmblALT  25925  volsup2  25927  mbfdm  25948  mbfima  25952  mbfid  25957  ismbfd  25961  mbfres2  25967  mbfposr  25974  mbfimaopnlem  25977  mbflimsup  25988  0plef  25994  i1f1lem  26011  itg11  26013  itg1addlem4  26021  i1fpos  26028  itg1le  26035  itg1climres  26036  mbfi1fseqlem5  26041  mbfi1flimlem  26044  xrge0f  26053  itg2ge0  26057  itg2seq  26064  itg2i1fseqle  26076  itg2i1fseq2  26078  itg2addlem  26080  itg2gt0  26082  limciun  26215  dvres  26232  dvres3a  26235  cpnres  26258  dvfre  26272  dvmptres3  26277  dvlip2  26316  dvgt0lem2  26324  deg1fvi  26404  uc1pmon1p  26471  fta1g  26489  ig1peu  26494  ig1pdvds  26499  plyco0  26511  plypf1  26532  dgrlem  26549  dgrub  26554  dgrlb  26556  coemulc  26575  plymul02  26602  plyreres  26605  plydivlem3  26617  plydivlem4  26618  plydiveu  26620  plyremlem  26626  fta1lem  26629  fta1  26630  vieta1lem2  26635  plyexmo  26637  elaa  26640  elqaalem3  26645  aannenlem1  26656  pserulm  26750  psercnlem2  26752  psercnlem1  26753  psercn  26754  abelth  26769  reeff1o  26775  pilem1  26779  recosf1o  26864  resinf1o  26865  efif1olem3  26873  efif1olem4  26874  efifo  26876  eff1olem  26877  ellogrn  26888  logcn  26976  dvloglem  26977  logf1o2  26979  efopnlem1  26985  efopnlem2  26986  efopn  26987  logtayl  26989  cxpcn3lem  27076  cxpcn3  27077  resqrtcn  27078  asinneg  27215  areambl  27287  emcllem7  27330  lgamgulm2  27364  basellem4  27412  sqff1o  27510  mpodvdsmulf1o  27522  fsumdvdsmul  27523  dvdsmulf1o  27524  ostthlem1  27955  ostth  27967  noetasuplem4  28094  madeval2  28220  elold  28246  old1  28252  madeoldsuc  28272  tglnfn  29011  tgplnfn  29254  f1otrg  29449  axlowdimlem6  29526  axlowdimlem8  29528  axlowdimlem9  29529  axlowdimlem11  29531  axlowdimlem12  29532  axlowdimlem17  29537  elntg2  29564  dfpth2  30315  cyclnumvtx  30389  crctcshlem4  30410  clwlkclwwlklem2  30592  eucrct2eupth  30847  ex-fpar  31064  cnnvm  31285  sspmlem  31335  nvo00  31364  nmlno0lem  31396  phoeqi  31460  ubthlem1  31473  hhip  31780  hhssabloilem  31864  hhssnv  31867  hhsssh  31872  occllem  31906  shsel  31917  chscllem2  32241  df0op2  32355  hoeq  32363  hocofni  32370  hoaddfni  32373  hosubfni  32374  hon0  32396  ho01i  32431  hoeq1  32433  elnlfn  32531  nmlnop0iALT  32598  lnopco0i  32607  imaelshi  32661  nlelchi  32664  rnbra  32710  cnvbraval  32713  kbass5  32723  hmopidmchi  32754  hmopidmpji  32755  foresf1o  33101  fcomptf  33253  ofpreima  33260  resf1o  33323  maprnin  33324  fpwrelmapffslem  33325  hashgt1  33401  indpreima  33433  s3clhash  33513  gsumpart  33625  xrge0tsmsd  33635  tocyc01  33680  cyc3evpm  33712  cycpmgcl  33715  cycpmconjslem2  33717  cyc3conja  33719  kerunit  33887  1arithidomlem1  34068  1arithidomlem2  34069  1arithidom  34070  psrmonmul  34183  dimval  34234  dimvalfi  34235  ply1degltdimlem  34255  ply1degltdim  34256  elirng  34319  txomap  34467  locfinreflem  34473  hauseqcn  34531  xpinpreima  34539  xpinpreima2  34540  tpr2rico  34545  mndpluscn  34559  raddcn  34562  xrge0pluscn  34573  xrge0tmdALT  34579  rge0scvg  34582  pl1cn  34588  elzrhunit  34610  qqhf  34619  cnrrext  34643  qqhre  34653  1stmbfm  34893  2ndmbfm  34894  mbfmcnt  34901  omssubadd  34933  carsggect  34951  eulerpartlemsv2  34991  eulerpartlems  34993  eulerpartlemv  34997  eulerpartlemb  35001  eulerpartlemf  35003  eulerpartlemt  35004  eulerpartlemmf  35008  eulerpartlemgvv  35009  eulerpartlemgh  35011  eulerpartlemgs2  35013  sseqmw  35024  sseqf  35025  sseqp1  35028  fiblem  35031  fibp1  35034  signsvtn0  35200  signstres  35205  signshlen  35220  reprinrn  35248  circlemethhgt  35273  txsconnlem  36006  iccllysconn  36016  rellysconn  36017  cvmseu  36042  cvmliftmolem2  36048  cvmliftlem6  36056  cvmliftlem7  36057  cvmliftlem8  36058  cvmliftlem9  36059  cvmliftlem11  36061  cvmliftlem15  36064  cvmlift2lem7  36075  cvmlift2lem10  36078  cvmlift3lem8  36092  cvmlift3lem9  36093  mvrsfpw  36272  mrsubff1  36280  msrid  36311  msrfo  36312  elmsta  36314  mtyf  36318  msubff1  36322  vhmcls  36332  mclsax  36335  elmthm  36342  mthmblem  36346  mclsppslem  36349  iprodefisumlem  36506  fullfunfnv  36711  fullfunfv  36712  tailfb  37166  filnetlem4  37170  regsfromunir1  37329  taupilem3  38242  icoreresf  38277  icoreelrnab  38279  relowlssretop  38288  relowlpssretop  38289  unccur  38528  ptrecube  38540  poimirlem28  38568  poimirlem32  38572  heicant  38575  opnmbllem0  38576  mblfinlem1  38577  mblfinlem2  38578  volsupnfl  38585  cnambfre  38588  dvtan  38590  itg2addnclem  38591  itg2addnclem2  38592  ftc1anclem3  38615  ftc1anclem5  38617  ftc1anclem7  38619  ftc1anclem8  38620  ftc1anc  38621  areacirc  38633  indexdom  38670  sdclem2  38678  sstotbnd2  38710  sstotbnd  38711  isbndx  38718  isbnd3b  38721  prdsbnd  38729  prdstotbnd  38730  ismtyhmeolem  38740  heibor1lem  38745  heiborlem1  38747  heibor  38757  rrnequiv  38771  keridl  38968  ellkr  40148  lkr0f  40153  cdleme50rnlem  41603  aks6d1c2lem4  43179  aks6d1c5  43191  sticksstones11  43208  sticksstones19  43217  sticksstones22  43220  aks6d1c6lem4  43225  aks6d1c6isolem2  43227  fsuppind  43620  elrfirn  43707  ismrcd2  43711  isnacs2  43718  nacsfix  43724  mapfzcons1  43729  mzpcompact2lem  43763  eq0rabdioph  43788  eldioph4b  43819  diophren  43821  pw2f1ocnv  44045  pw2f1o2val2  44048  lmhmfgsplit  44089  pwssplit4  44092  hbt  44133  mpaaeu  44153  mendring  44191  proot1mul  44197  proot1hash  44198  proot1ex  44199  deg1mhm  44203  fgraphopab  44206  hausgraph  44208  nvocnvb  44424  ofsubid  45309  expgrowthi  45318  expgrowth  45320  binomcxplemdvbinom  45338  binomcxplemcvg  45339  binomcxplemnotnn0  45341  relpfrlem  45944  rfcnpre1  46037  rfcnpre2  46049  cncmpmax  46050  rfcnpre3  46051  rfcnpre4  46052  elixpconstg  46105  ffi  46189  islptre  46632  resincncf  46886  dvcosre  46923  dvresntr  46929  volioof  46998  stoweidlem48  47059  fourierdlem12  47130  fourierdlem15  47133  fourierdlem41  47159  fourierdlem42  47160  fourierdlem46  47163  fourierdlem54  47171  fourierdlem56  47173  fourierdlem62  47179  fourierdlem64  47181  fourierdlem65  47182  fourierdlem73  47190  fourierdlem74  47191  fourierdlem75  47192  fourierdlem102  47219  fourierdlem103  47220  fourierdlem104  47221  fourierdlem114  47231  sge0split  47420  elhoi  47553  mbfresmf  47750  cjnpoly  47940  cfsetsnfsetf1  48130  cfsetsnfsetfo  48131  focofob  48151  f1ocof1ob  48152  fafvelcdm  48241  ffnafv  48242  fafv2elcdm  48305  fafv2elrnb  48306  imarnf1pr  48353  2ffzoeq  48399  fundcmpsurbijinjpreimafv  48490  fundcmpsurinjimaid  48494  fargshiftfv  48522  fargshiftf  48523  fargshiftf1  48524  fargshiftfo  48525  cycl3grtri  49046  fdmdifeqresdif  49455  fdivmpt  49653  fdivmptf  49654  refdivmptf  49655  1arymaptf1  49755  2arymaptf1  49766  ackfnnn0  49798  homf0  50118  aacllem  50940