Theorem ffn 6686

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

Syntax hints:   → wi 4   ⊆ wss 3902  ran crn 5644   Fn wfn 6511  ⟶wf 6512

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 209  df-an 400  df-f 6520

This theorem is referenced by:  ffnd  6687  ffun  6689  ffunOLD  6690  frel  6692  fdm  6696  ffrn  6700  fresin  6728  fresaun  6730  fresaunres2  6731  fcoi1  6733  feu  6735  f0bi  6742  dffo2  6777  fimadmfo  6782  fdmeu  6918  feqmptdf  6932  fimarab  6936  fvco3  6962  ffvelcdm  7057  dff2  7075  dffo3  7078  dffo4  7079  dffo5  7080  dffo3f  7082  f1ompt  7087  ffnfv  7095  fcdmssb  7098  fcompt  7110  fsn2  7113  fprb  7173  fconst2g  7182  fpr2g  7190  fex  7205  dff13  7233  nvocnv  7260  soisores  7306  fdmexb  7883  resf1extb  7910  fo1stres  7991  fo2ndres  7992  1stcof  7995  2ndcof  7996  curry1f  8079  curry2f  8081  fparlem1  8085  fparlem2  8086  fo2ndf  8094  soseq  8133  tposf2  8224  smo11  8329  fsetexb  8839  mapsnd  8862  pw2f1olem  9047  mapen  9107  mapunen  9112  fissuni  9294  fipreima  9295  indexfi  9297  mapfien  9348  oismo  9482  cantnflt  9621  cantnfp1lem3  9629  cantnflem4  9641  tcrank  9836  updjudhcoinlf  9884  updjudhcoinrg  9885  updjud  9886  infpwfien  10012  cardinfima  10047  dfacacn  10092  cfflb  10210  cofsmo  10220  cfcoflem  10223  coftr  10224  fin23lem40  10302  axdc3lem2  10402  ac6num  10430  ac6c4  10432  ac6s2  10437  ttukeylem6  10465  iunfo  10490  pwcfsdom  10535  fpwwe2lem5  10587  fpwwe2lem7  10589  pwfseqlem3  10612  inar1  10727  tskcard  10733  tskuni  10735  tskurn  10741  gruima  10754  nqerrel  10884  recmulnq  10916  dmrecnq  10920  axpre-sup  11121  ofsubeq0  12186  indpi1  12203  dfz2  12581  uzn0  12850  rpnnen1lem3  12974  rpnnen1lem5  12976  unirnioo  13447  dfioo2  13448  ioorebas  13449  fseq1p1m1  13597  2ffzeq  13648  fvinim0ffz  13789  injresinjlem  13790  fsequb2  13983  fseqsupcl  13984  fseqsupubi  13985  ser0f  14062  hashgval  14340  hashinf  14342  hashresfn  14347  ffz0hash  14454  fnfzo0hash  14457  wrdred1hash  14568  revlen  14769  revrev  14774  repswlen  14783  repsdf2  14785  cshword  14798  0csh0  14800  lenco  14839  s1co  14840  cshco  14843  swrdco  14844  s7f1o  14973  ofccat  14976  shftf  15086  uzin2  15363  rexanuz  15364  limsuple  15496  limsupval2  15498  rlimres  15576  lo1res  15577  rlimresb  15583  isercolllem2  15684  isercolllem3  15685  isercoll  15686  supcvg  15877  prodf1f  15913  eff2  16122  reeff1  16143  tanval  16151  ruclem4  16257  ruclem12  16264  prmreclem6  16948  1arithlem4  16953  1arith  16954  vdwmc  17005  vdwlem1  17008  vdwlem8  17015  vdwlem13  17020  ramval  17035  0ram  17047  0ram2  17048  0ramcl  17050  ramcl  17056  fsets  17196  firest  17452  0ssc  17861  0subcat  17862  isfull2  17937  arwhoma  18069  gsumval2a  18710  isgrpinv  19026  kerf1ghm  19278  f1omvdconj  19477  pmtrmvd  19487  pmtrfinv  19492  pmtrdifellem4  19510  efgsfo  19770  efgredlem  19778  efgcpbllemb  19786  frgpup3lem  19808  0frgp  19810  gexex  19884  torsubg  19885  gsumval3  19938  gsumzres  19940  gsummptmhm  19971  gsumzoppg  19975  dprdf1o  20065  dprd2db  20076  zrinitorngc  20679  zrtermorngc  20680  zrtermoringc  20712  srngf1o  20885  lmhmima  21102  lmhmpreima  21103  lmhmrnlss  21105  lspextmo  21111  pwssplit1  21114  cnfldadd  21418  cnfldmul  21420  cnfldplusf  21439  cnfldsub  21440  chrrhm  21571  znunit  21603  psgnevpmb  21627  psgndiflemB  21640  mpofrlmd  21817  frlmipval  21819  frlmphl  21821  frlmlbs  21837  frlmup4  21841  ellspd  21842  lindfmm  21867  lsslindf  21870  psrbaglefi  21966  psrlidm  22001  mplmonmul  22077  evlseu  22124  mpfconst  22150  mpfproj  22151  mpfsubrg  22152  coe1sclmulfv  22334  pf1const  22397  pf1id  22398  pf1subrg  22399  mpfpf1  22402  pf1mpf  22403  mamuass  22450  mamudi  22451  mamudir  22452  mamuvs1  22453  mamuvs2  22454  1mavmul  22596  mavmulass  22597  mdetunilem7  22666  madutpos  22690  lecldbas  23267  lmbr2  23307  cncnpi  23326  cncnp  23328  cnpdis  23341  lmff  23349  pnrmopn  23391  dnsconst  23426  cmpsub  23448  tgcmp  23449  hauscmplem  23454  2ndcctbss  23503  2ndcomap  23506  2ndcsep  23507  1stccnp  23510  kgenidm  23595  iskgen2  23596  1stckgen  23602  kgen2cn  23607  ptpjpre1  23619  pttop  23630  ptuni  23642  ptval2  23649  tx1cn  23657  tx2cn  23658  ptpjcn  23659  ptpjopn  23660  ptclsg  23663  ptcnplem  23669  upxp  23671  txcnmpt  23672  uptx  23673  txcmplem2  23690  txkgen  23700  xkoptsub  23702  xkopt  23703  xkococnlem  23707  xkococn  23708  ptcmpfi  23861  zfbas  23944  uzrest  23945  rnelfmlem  24000  rnelfm  24001  fmfnfmlem2  24003  fmfnfm  24006  lmflf  24053  alexsubALT  24099  clssubg  24157  qustgplem  24169  tsmsres  24192  tsmsxplem1  24201  ucncn  24332  xmettpos  24397  imasdsf1olem  24421  blrnps  24456  blrn  24457  xmeterval  24480  tmslem  24530  tmsxms  24534  imasf1oxms  24537  prdsxms  24578  blval2  24610  metuel2  24613  isngp2  24645  isngp3  24646  tngngp2  24700  isnghm  24771  qtopbaslem  24806  qdensere  24817  cnbl0  24821  cnblcld  24822  cnfldms  24823  blssioo  24843  tgioo  24844  tgqioo  24848  xrtgioo  24855  xrsdsre  24859  xrge0tsms  24883  bndth  25008  lebnumlem3  25013  nmhmcn  25170  cphsqrtcl  25234  lmmbr2  25309  caucfil  25333  causs  25348  lmcau  25363  bcth3  25381  cncms  25405  cnfldcusp  25407  rrxmvallem  25454  ivthicc  25508  ovolfioo  25517  ovolficc  25518  ovolficcss  25519  ovollb2lem  25538  ovoliunlem2  25553  ovolshftlem1  25559  ovolicc2  25572  ismbl  25576  voliunlem2  25601  volsup  25606  ioorf  25623  ioorinv  25626  ioorcl  25627  uniiccdif  25628  uniioovol  25629  uniiccvol  25630  uniioombllem2  25633  uniioombllem4  25636  dyaddisj  25646  dyadmax  25648  dyadmbllem  25649  dyadmbl  25650  opnmbllem  25651  opnmblALT  25653  volsup2  25655  mbfdm  25676  mbfima  25680  mbfid  25685  ismbfd  25689  mbfres2  25695  mbfposr  25702  mbfimaopnlem  25705  mbflimsup  25716  0plef  25722  i1f1lem  25739  itg11  25741  itg1addlem4  25749  i1fpos  25756  itg1le  25763  itg1climres  25764  mbfi1fseqlem5  25769  mbfi1flimlem  25772  xrge0f  25781  itg2ge0  25785  itg2seq  25792  itg2i1fseqle  25804  itg2i1fseq2  25806  itg2addlem  25808  itg2gt0  25810  limciun  25944  dvres  25961  dvres3a  25964  cpnres  25987  dvfre  26001  dvmptres3  26006  dvlip2  26045  dvgt0lem2  26053  deg1fvi  26133  uc1pmon1p  26200  fta1g  26218  ig1peu  26223  ig1pdvds  26228  plyco0  26240  plypf1  26260  dgrlem  26277  dgrub  26282  dgrlb  26284  coemulc  26303  plymul02  26332  plyreres  26335  plydivlem3  26347  plydivlem4  26348  plydiveu  26350  plyremlem  26356  fta1lem  26359  fta1  26360  vieta1lem2  26363  plyexmo  26365  elaa  26368  elqaalem3  26373  aannenlem1  26380  pserulm  26473  psercnlem2  26475  psercnlem1  26476  psercn  26477  abelth  26492  reeff1o  26498  pilem1  26502  recosf1o  26588  resinf1o  26589  efif1olem3  26597  efif1olem4  26598  efifo  26600  eff1olem  26601  ellogrn  26612  logcn  26700  dvloglem  26701  logf1o2  26703  efopnlem1  26709  efopnlem2  26710  efopn  26711  logtayl  26713  cxpcn3lem  26800  cxpcn3  26801  resqrtcn  26802  asinneg  26939  areambl  27011  emcllem7  27054  lgamgulm2  27088  basellem4  27136  sqff1o  27234  mpodvdsmulf1o  27246  fsumdvdsmul  27247  dvdsmulf1o  27248  ostthlem1  27679  ostth  27691  noetasuplem4  27788  madeval2  27914  elold  27940  old1  27946  madeoldsuc  27966  tglnfn  28704  f1otrg  29028  axlowdimlem6  29105  axlowdimlem8  29107  axlowdimlem9  29108  axlowdimlem11  29110  axlowdimlem12  29111  axlowdimlem17  29116  elntg2  29143  dfpth2  29886  cyclnumvtx  29957  crctcshlem4  29977  clwlkclwwlklem2  30159  eucrct2eupth  30404  ex-fpar  30621  cnnvm  30842  sspmlem  30892  nvo00  30921  nmlno0lem  30953  phoeqi  31017  ubthlem1  31030  hhip  31337  hhssabloilem  31421  hhssnv  31424  hhsssh  31429  occllem  31463  shsel  31474  chscllem2  31798  df0op2  31912  hoeq  31920  hocofni  31927  hoaddfni  31930  hosubfni  31931  hon0  31953  ho01i  31988  hoeq1  31990  elnlfn  32088  nmlnop0iALT  32155  lnopco0i  32164  imaelshi  32218  nlelchi  32221  rnbra  32267  cnvbraval  32270  kbass5  32280  hmopidmchi  32311  hmopidmpji  32312  foresf1o  32663  fcomptf  32821  ofpreima  32828  resf1o  32893  maprnin  32894  fpwrelmapffslem  32895  hashgt1  32971  indpreima  33004  s3clhash  33087  gsumpart  33204  xrge0tsmsd  33214  tocyc01  33259  cyc3evpm  33291  cycpmgcl  33294  cycpmconjslem2  33296  cyc3conja  33298  kerunit  33472  1arithidomlem1  33692  1arithidomlem2  33693  1arithidom  33694  psrmonmul  33808  dimval  33859  dimvalfi  33860  ply1degltdimlem  33880  ply1degltdim  33881  elirng  33944  txomap  34092  locfinreflem  34098  hauseqcn  34156  xpinpreima  34164  xpinpreima2  34165  tpr2rico  34170  mndpluscn  34184  raddcn  34187  xrge0pluscn  34198  xrge0tmdALT  34204  rge0scvg  34207  pl1cn  34213  elzrhunit  34235  qqhf  34244  cnrrext  34268  qqhre  34278  1stmbfm  34518  2ndmbfm  34519  mbfmcnt  34526  omssubadd  34558  carsggect  34576  eulerpartlemsv2  34616  eulerpartlems  34618  eulerpartlemv  34622  eulerpartlemb  34626  eulerpartlemf  34628  eulerpartlemt  34629  eulerpartlemmf  34633  eulerpartlemgvv  34634  eulerpartlemgh  34636  eulerpartlemgs2  34638  sseqmw  34649  sseqf  34650  sseqp1  34653  fiblem  34656  fibp1  34659  signsvtn0  34825  signstres  34830  signshlen  34845  reprinrn  34873  circlemethhgt  34898  txsconnlem  35551  iccllysconn  35561  rellysconn  35562  cvmseu  35587  cvmliftmolem2  35593  cvmliftlem6  35601  cvmliftlem7  35602  cvmliftlem8  35603  cvmliftlem9  35604  cvmliftlem11  35606  cvmliftlem15  35609  cvmlift2lem7  35620  cvmlift2lem10  35623  cvmlift3lem8  35637  cvmlift3lem9  35638  mvrsfpw  35817  mrsubff1  35825  msrid  35856  msrfo  35857  elmsta  35859  mtyf  35863  msubff1  35867  vhmcls  35877  mclsax  35880  elmthm  35887  mthmblem  35891  mclsppslem  35894  iprodefisumlem  36051  fullfunfnv  36257  fullfunfv  36258  tailfb  36698  filnetlem4  36702  regsfromunir1  36861  taupilem3  37772  icoreresf  37807  icoreelrnab  37809  relowlssretop  37818  relowlpssretop  37819  unccur  38063  matunitlindflem1  38076  matunitlindflem2  38077  ptrecube  38080  poimirlem28  38108  poimirlem32  38112  heicant  38115  opnmbllem0  38116  mblfinlem1  38117  mblfinlem2  38118  volsupnfl  38125  cnambfre  38128  dvtan  38130  itg2addnclem  38131  itg2addnclem2  38132  ftc1anclem3  38155  ftc1anclem5  38157  ftc1anclem7  38159  ftc1anclem8  38160  ftc1anc  38161  areacirc  38173  indexdom  38194  sdclem2  38202  sstotbnd2  38234  sstotbnd  38235  isbndx  38242  isbnd3b  38245  prdsbnd  38253  prdstotbnd  38254  ismtyhmeolem  38264  heibor1lem  38269  heiborlem1  38271  heibor  38281  rrnequiv  38295  keridl  38492  ellkr  39674  lkr0f  39679  cdleme50rnlem  41129  aks6d1c2lem4  42705  aks6d1c5  42717  sticksstones11  42734  sticksstones19  42743  sticksstones22  42746  aks6d1c6lem4  42751  aks6d1c6isolem2  42753  fsuppind  43133  elrfirn  43237  ismrcd2  43241  isnacs2  43248  nacsfix  43254  mapfzcons1  43259  mzpcompact2lem  43293  eq0rabdioph  43318  eldioph4b  43349  diophren  43351  pw2f1ocnv  43575  pw2f1o2val2  43578  lmhmfgsplit  43624  pwssplit4  43627  hbt  43668  mpaaeu  43688  mendring  43726  proot1mul  43732  proot1hash  43733  proot1ex  43734  deg1mhm  43738  fgraphopab  43741  hausgraph  43743  nvocnvb  43959  ofsubid  44861  expgrowthi  44870  expgrowth  44872  binomcxplemdvbinom  44890  binomcxplemcvg  44891  binomcxplemnotnn0  44893  relpfrlem  45490  rfcnpre1  45560  rfcnpre2  45572  cncmpmax  45573  rfcnpre3  45574  rfcnpre4  45575  elixpconstg  45628  ffi  45712  islptre  46156  resincncf  46410  dvcosre  46447  dvresntr  46453  volioof  46522  stoweidlem48  46583  fourierdlem12  46654  fourierdlem15  46657  fourierdlem41  46683  fourierdlem42  46684  fourierdlem46  46687  fourierdlem54  46695  fourierdlem56  46697  fourierdlem62  46703  fourierdlem64  46705  fourierdlem65  46706  fourierdlem73  46714  fourierdlem74  46715  fourierdlem75  46716  fourierdlem102  46743  fourierdlem103  46744  fourierdlem104  46745  fourierdlem114  46755  sge0split  46944  elhoi  47077  mbfresmf  47274  cjnpoly  47444  cfsetsnfsetf1  47614  cfsetsnfsetfo  47615  focofob  47635  f1ocof1ob  47636  fafvelcdm  47725  ffnafv  47726  fafv2elcdm  47789  fafv2elrnb  47790  imarnf1pr  47837  2ffzoeq  47883  fundcmpsurbijinjpreimafv  47974  fundcmpsurinjimaid  47978  fargshiftfv  48006  fargshiftf  48007  fargshiftf1  48008  fargshiftfo  48009  cycl3grtri  48530  fdmdifeqresdif  48925  fdivmpt  49123  fdivmptf  49124  refdivmptf  49125  1arymaptf1  49225  2arymaptf1  49236  ackfnnn0  49268  homf0  49591  aacllem  50383