Theorem ffn 6703

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

Syntax hints:   → wi 4   ⊆ wss 3913  ran crn 5660   Fn wfn 6529  ⟶wf 6530

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 210  df-an 401  df-f 6538

This theorem is referenced by:  ffnd  6704  ffun  6706  ffunOLD  6707  frel  6709  fdm  6713  ffrn  6717  fresin  6745  fresaun  6747  fresaunres2  6748  fcoi1  6750  feu  6752  f0bi  6759  dffo2  6794  fimadmfo  6799  fdmeu  6935  feqmptdf  6949  fimarab  6953  fvco3  6979  ffvelcdm  7074  dff2  7092  dffo3  7095  dffo4  7096  dffo5  7097  dffo3f  7099  f1ompt  7104  ffnfv  7112  fcdmssb  7115  fcompt  7127  fsn2  7130  fprb  7190  fconst2g  7199  fpr2g  7207  fex  7222  dff13  7250  nvocnv  7277  soisores  7323  fdmexb  7900  resf1extb  7927  fo1stres  8008  fo2ndres  8009  1stcof  8012  2ndcof  8013  curry1f  8097  curry2f  8099  fparlem1  8103  fparlem2  8104  fo2ndf  8112  soseq  8151  tposf2  8242  smo11  8347  fsetexb  8857  mapsnd  8880  pw2f1olem  9065  mapen  9125  mapunen  9130  fissuni  9310  fipreima  9311  indexfi  9313  mapfien  9364  oismo  9498  cantnflt  9637  cantnfp1lem3  9645  cantnflem4  9657  tcrank  9852  updjudhcoinlf  9914  updjudhcoinrg  9915  updjud  9916  infpwfien  10042  cardinfima  10077  dfacacn  10121  cfflb  10239  cofsmo  10249  cfcoflem  10252  coftr  10253  fin23lem40  10331  axdc3lem2  10431  ac6num  10459  ac6c4  10461  ac6s2  10466  ttukeylem6  10494  iunfo  10519  pwcfsdom  10564  fpwwe2lem5  10616  fpwwe2lem7  10618  pwfseqlem3  10641  inar1  10756  tskcard  10762  tskuni  10764  tskurn  10770  gruima  10783  nqerrel  10913  recmulnq  10945  dmrecnq  10949  axpre-sup  11150  ofsubeq0  12211  indpi1  12228  dfz2  12606  uzn0  12875  rpnnen1lem3  12999  rpnnen1lem5  13001  unirnioo  13472  dfioo2  13473  ioorebas  13474  fseq1p1m1  13622  2ffzeq  13673  fvinim0ffz  13814  injresinjlem  13815  fsequb2  14008  fseqsupcl  14009  fseqsupubi  14010  ser0f  14087  hashgval  14365  hashinf  14367  hashresfn  14372  ffz0hash  14480  fnfzo0hash  14483  wrdred1hash  14594  revlen  14795  revrev  14800  repswlen  14809  repsdf2  14811  cshword  14824  0csh0  14826  lenco  14865  s1co  14866  cshco  14869  swrdco  14870  s7f1o  14999  ofccat  15002  shftf  15112  uzin2  15392  rexanuz  15393  limsuple  15525  limsupval2  15527  rlimres  15605  lo1res  15606  rlimresb  15612  isercolllem2  15713  isercolllem3  15714  isercoll  15715  supcvg  15906  prodf1f  15942  eff2  16151  reeff1  16172  tanval  16180  ruclem4  16286  ruclem12  16293  prmreclem6  16977  1arithlem4  16982  1arith  16983  vdwmc  17034  vdwlem1  17037  vdwlem8  17044  vdwlem13  17049  ramval  17064  0ram  17076  0ram2  17077  0ramcl  17079  ramcl  17085  fsets  17225  firest  17481  0ssc  17890  0subcat  17891  isfull2  17966  arwhoma  18098  gsumval2a  18739  isgrpinv  19056  kerf1ghm  19313  f1omvdconj  19512  pmtrmvd  19522  pmtrfinv  19527  pmtrdifellem4  19545  efgsfo  19805  efgredlem  19813  efgcpbllemb  19821  frgpup3lem  19843  0frgp  19845  gexex  19919  torsubg  19920  gsumval3  19973  gsumzres  19975  gsummptmhm  20006  gsumzoppg  20010  dprdf1o  20100  dprd2db  20111  zrinitorngc  20723  zrtermorngc  20724  zrtermoringc  20756  srngf1o  20925  lmhmima  21142  lmhmpreima  21143  lmhmrnlss  21145  lspextmo  21151  pwssplit1  21154  cnfldadd  21493  cnfldmul  21495  cnfldplusf  21514  cnfldsub  21515  chrrhm  21646  znunit  21678  psgnevpmb  21702  psgndiflemB  21715  mpofrlmd  21892  frlmipval  21894  frlmphl  21896  frlmlbs  21912  frlmup4  21916  ellspd  21917  lindfmm  21942  lsslindf  21945  psrbaglefi  22041  psrlidm  22076  mplmonmul  22152  evlseu  22199  mpfconst  22225  mpfproj  22226  mpfsubrg  22227  coe1sclmulfv  22409  pf1const  22471  pf1id  22472  pf1subrg  22473  mpfpf1  22476  pf1mpf  22477  mamuass  22524  mamudi  22525  mamudir  22526  mamuvs1  22527  mamuvs2  22528  1mavmul  22670  mavmulass  22671  mdetunilem7  22740  madutpos  22764  lecldbas  23341  lmbr2  23381  cncnpi  23400  cncnp  23402  cnpdis  23415  lmff  23423  pnrmopn  23465  dnsconst  23500  cmpsub  23522  tgcmp  23523  hauscmplem  23528  2ndcctbss  23577  2ndcomap  23580  2ndcsep  23581  1stccnp  23584  kgenidm  23669  iskgen2  23670  1stckgen  23676  kgen2cn  23681  ptpjpre1  23693  pttop  23704  ptuni  23716  ptval2  23723  tx1cn  23731  tx2cn  23732  ptpjcn  23733  ptpjopn  23734  ptclsg  23737  ptcnplem  23743  upxp  23745  txcnmpt  23746  uptx  23747  txcmplem2  23764  txkgen  23774  xkoptsub  23776  xkopt  23777  xkococnlem  23781  xkococn  23782  ptcmpfi  23935  zfbas  24018  uzrest  24019  rnelfmlem  24074  rnelfm  24075  fmfnfmlem2  24077  fmfnfm  24080  lmflf  24127  alexsubALT  24173  clssubg  24231  qustgplem  24243  tsmsres  24266  tsmsxplem1  24275  ucncn  24406  xmettpos  24471  imasdsf1olem  24495  blrnps  24530  blrn  24531  xmeterval  24554  tmslem  24604  tmsxms  24608  imasf1oxms  24611  prdsxms  24652  blval2  24684  metuel2  24687  isngp2  24719  isngp3  24720  tngngp2  24774  isnghm  24845  qtopbaslem  24880  qdensere  24891  cnbl0  24895  cnblcld  24896  cnfldms  24897  blssioo  24917  tgioo  24918  tgqioo  24922  xrtgioo  24929  xrsdsre  24933  xrge0tsms  24957  bndth  25082  lebnumlem3  25087  nmhmcn  25244  cphsqrtcl  25308  lmmbr2  25383  caucfil  25407  causs  25422  lmcau  25437  bcth3  25455  cncms  25479  cnfldcusp  25481  rrxmvallem  25528  ivthicc  25582  ovolfioo  25591  ovolficc  25592  ovolficcss  25593  ovollb2lem  25612  ovoliunlem2  25627  ovolshftlem1  25633  ovolicc2  25646  ismbl  25650  voliunlem2  25675  volsup  25680  ioorf  25697  ioorinv  25700  ioorcl  25701  uniiccdif  25702  uniioovol  25703  uniiccvol  25704  uniioombllem2  25707  uniioombllem4  25710  dyaddisj  25720  dyadmax  25722  dyadmbllem  25723  dyadmbl  25724  opnmbllem  25725  opnmblALT  25727  volsup2  25729  mbfdm  25750  mbfima  25754  mbfid  25759  ismbfd  25763  mbfres2  25769  mbfposr  25776  mbfimaopnlem  25779  mbflimsup  25790  0plef  25796  i1f1lem  25813  itg11  25815  itg1addlem4  25823  i1fpos  25830  itg1le  25837  itg1climres  25838  mbfi1fseqlem5  25843  mbfi1flimlem  25846  xrge0f  25855  itg2ge0  25859  itg2seq  25866  itg2i1fseqle  25878  itg2i1fseq2  25880  itg2addlem  25882  itg2gt0  25884  limciun  26018  dvres  26035  dvres3a  26038  cpnres  26061  dvfre  26075  dvmptres3  26080  dvlip2  26119  dvgt0lem2  26127  deg1fvi  26207  uc1pmon1p  26274  fta1g  26292  ig1peu  26297  ig1pdvds  26302  plyco0  26314  plypf1  26334  dgrlem  26351  dgrub  26356  dgrlb  26358  coemulc  26377  plymul02  26406  plyreres  26409  plydivlem3  26421  plydivlem4  26422  plydiveu  26424  plyremlem  26430  fta1lem  26433  fta1  26434  vieta1lem2  26437  plyexmo  26439  elaa  26442  elqaalem3  26447  aannenlem1  26454  pserulm  26547  psercnlem2  26549  psercnlem1  26550  psercn  26551  abelth  26566  reeff1o  26572  pilem1  26576  recosf1o  26662  resinf1o  26663  efif1olem3  26671  efif1olem4  26672  efifo  26674  eff1olem  26675  ellogrn  26686  logcn  26774  dvloglem  26775  logf1o2  26777  efopnlem1  26783  efopnlem2  26784  efopn  26785  logtayl  26787  cxpcn3lem  26874  cxpcn3  26875  resqrtcn  26876  asinneg  27013  areambl  27085  emcllem7  27128  lgamgulm2  27162  basellem4  27210  sqff1o  27308  mpodvdsmulf1o  27320  fsumdvdsmul  27321  dvdsmulf1o  27322  ostthlem1  27753  ostth  27765  noetasuplem4  27862  madeval2  27988  elold  28014  old1  28020  madeoldsuc  28040  tglnfn  28778  tgplnfn  29011  f1otrg  29157  axlowdimlem6  29234  axlowdimlem8  29236  axlowdimlem9  29237  axlowdimlem11  29239  axlowdimlem12  29240  axlowdimlem17  29245  elntg2  29272  dfpth2  30015  cyclnumvtx  30086  crctcshlem4  30106  clwlkclwwlklem2  30288  eucrct2eupth  30533  ex-fpar  30750  cnnvm  30971  sspmlem  31021  nvo00  31050  nmlno0lem  31082  phoeqi  31146  ubthlem1  31159  hhip  31466  hhssabloilem  31550  hhssnv  31553  hhsssh  31558  occllem  31592  shsel  31603  chscllem2  31927  df0op2  32041  hoeq  32049  hocofni  32056  hoaddfni  32059  hosubfni  32060  hon0  32082  ho01i  32117  hoeq1  32119  elnlfn  32217  nmlnop0iALT  32284  lnopco0i  32293  imaelshi  32347  nlelchi  32350  rnbra  32396  cnvbraval  32399  kbass5  32409  hmopidmchi  32440  hmopidmpji  32441  foresf1o  32787  fcomptf  32940  ofpreima  32947  resf1o  33012  maprnin  33013  fpwrelmapffslem  33014  hashgt1  33090  indpreima  33122  s3clhash  33205  gsumpart  33320  xrge0tsmsd  33330  tocyc01  33375  cyc3evpm  33407  cycpmgcl  33410  cycpmconjslem2  33412  cyc3conja  33414  kerunit  33584  1arithidomlem1  33766  1arithidomlem2  33767  1arithidom  33768  psrmonmul  33881  dimval  33932  dimvalfi  33933  ply1degltdimlem  33953  ply1degltdim  33954  elirng  34017  txomap  34165  locfinreflem  34171  hauseqcn  34229  xpinpreima  34237  xpinpreima2  34238  tpr2rico  34243  mndpluscn  34257  raddcn  34260  xrge0pluscn  34271  xrge0tmdALT  34277  rge0scvg  34280  pl1cn  34286  elzrhunit  34308  qqhf  34317  cnrrext  34341  qqhre  34351  1stmbfm  34591  2ndmbfm  34592  mbfmcnt  34599  omssubadd  34631  carsggect  34649  eulerpartlemsv2  34689  eulerpartlems  34691  eulerpartlemv  34695  eulerpartlemb  34699  eulerpartlemf  34701  eulerpartlemt  34702  eulerpartlemmf  34706  eulerpartlemgvv  34707  eulerpartlemgh  34709  eulerpartlemgs2  34711  sseqmw  34722  sseqf  34723  sseqp1  34726  fiblem  34729  fibp1  34732  signsvtn0  34898  signstres  34903  signshlen  34918  reprinrn  34946  circlemethhgt  34971  txsconnlem  35627  iccllysconn  35637  rellysconn  35638  cvmseu  35663  cvmliftmolem2  35669  cvmliftlem6  35677  cvmliftlem7  35678  cvmliftlem8  35679  cvmliftlem9  35680  cvmliftlem11  35682  cvmliftlem15  35685  cvmlift2lem7  35696  cvmlift2lem10  35699  cvmlift3lem8  35713  cvmlift3lem9  35714  mvrsfpw  35893  mrsubff1  35901  msrid  35932  msrfo  35933  elmsta  35935  mtyf  35939  msubff1  35943  vhmcls  35953  mclsax  35956  elmthm  35963  mthmblem  35967  mclsppslem  35970  iprodefisumlem  36127  fullfunfnv  36333  fullfunfv  36334  tailfb  36773  filnetlem4  36777  regsfromunir1  36936  taupilem3  37846  icoreresf  37881  icoreelrnab  37883  relowlssretop  37892  relowlpssretop  37893  unccur  38137  matunitlindflem1  38150  matunitlindflem2  38151  ptrecube  38154  poimirlem28  38182  poimirlem32  38186  heicant  38189  opnmbllem0  38190  mblfinlem1  38191  mblfinlem2  38192  volsupnfl  38199  cnambfre  38202  dvtan  38204  itg2addnclem  38205  itg2addnclem2  38206  ftc1anclem3  38229  ftc1anclem5  38231  ftc1anclem7  38233  ftc1anclem8  38234  ftc1anc  38235  areacirc  38247  indexdom  38268  sdclem2  38276  sstotbnd2  38308  sstotbnd  38309  isbndx  38316  isbnd3b  38319  prdsbnd  38327  prdstotbnd  38328  ismtyhmeolem  38338  heibor1lem  38343  heiborlem1  38345  heibor  38355  rrnequiv  38369  keridl  38566  ellkr  39748  lkr0f  39753  cdleme50rnlem  41203  aks6d1c2lem4  42779  aks6d1c5  42791  sticksstones11  42808  sticksstones19  42817  sticksstones22  42820  aks6d1c6lem4  42825  aks6d1c6isolem2  42827  fsuppind  43209  elrfirn  43313  ismrcd2  43317  isnacs2  43324  nacsfix  43330  mapfzcons1  43335  mzpcompact2lem  43369  eq0rabdioph  43394  eldioph4b  43425  diophren  43427  pw2f1ocnv  43651  pw2f1o2val2  43654  lmhmfgsplit  43700  pwssplit4  43703  hbt  43744  mpaaeu  43764  mendring  43802  proot1mul  43808  proot1hash  43809  proot1ex  43810  deg1mhm  43814  fgraphopab  43817  hausgraph  43819  nvocnvb  44035  ofsubid  44921  expgrowthi  44930  expgrowth  44932  binomcxplemdvbinom  44950  binomcxplemcvg  44951  binomcxplemnotnn0  44953  relpfrlem  45549  rfcnpre1  45626  rfcnpre2  45638  cncmpmax  45639  rfcnpre3  45640  rfcnpre4  45641  elixpconstg  45694  ffi  45778  islptre  46222  resincncf  46476  dvcosre  46513  dvresntr  46519  volioof  46588  stoweidlem48  46649  fourierdlem12  46720  fourierdlem15  46723  fourierdlem41  46749  fourierdlem42  46750  fourierdlem46  46753  fourierdlem54  46761  fourierdlem56  46763  fourierdlem62  46769  fourierdlem64  46771  fourierdlem65  46772  fourierdlem73  46780  fourierdlem74  46781  fourierdlem75  46782  fourierdlem102  46809  fourierdlem103  46810  fourierdlem104  46811  fourierdlem114  46821  sge0split  47010  elhoi  47143  mbfresmf  47340  cjnpoly  47510  cfsetsnfsetf1  47680  cfsetsnfsetfo  47681  focofob  47701  f1ocof1ob  47702  fafvelcdm  47791  ffnafv  47792  fafv2elcdm  47855  fafv2elrnb  47856  imarnf1pr  47903  2ffzoeq  47949  fundcmpsurbijinjpreimafv  48040  fundcmpsurinjimaid  48044  fargshiftfv  48072  fargshiftf  48073  fargshiftf1  48074  fargshiftfo  48075  cycl3grtri  48596  fdmdifeqresdif  49002  fdivmpt  49200  fdivmptf  49201  refdivmptf  49202  1arymaptf1  49302  2arymaptf1  49313  ackfnnn0  49345  homf0  49667  aacllem  50470