Theorem ffn 6670

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

Syntax hints:   → wi 4   ⊆ wss 3911  ran crn 5632   Fn wfn 6494  ⟶wf 6495

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 207  df-an 396  df-f 6503

This theorem is referenced by:  ffnd  6671  ffun  6673  frel  6675  fdm  6679  ffrn  6683  fresin  6711  fresaun  6713  fresaunres2  6714  fcoi1  6716  feu  6718  f0bi  6725  dffo2  6758  fimadmfo  6763  fdmeu  6899  feqmptdf  6913  fimarab  6917  fvco3  6942  ffvelcdm  7035  dff2  7053  dffo3  7056  dffo4  7057  dffo5  7058  dffo3f  7060  f1ompt  7065  ffnfv  7073  fcdmssb  7076  fcompt  7087  fsn2  7090  fprb  7150  fconst2g  7159  fpr2g  7167  fex  7182  dff13  7211  nvocnv  7238  soisores  7284  fdmexb  7863  resf1extb  7890  fo1stres  7973  fo2ndres  7974  1stcof  7977  2ndcof  7978  curry1f  8062  curry2f  8064  fparlem1  8068  fparlem2  8069  fo2ndf  8077  soseq  8115  tposf2  8206  smo11  8310  fsetexb  8814  mapsnd  8836  pw2f1olem  9022  mapen  9082  mapunen  9087  fissuni  9284  fipreima  9285  indexfi  9287  mapfien  9335  oismo  9469  cantnflt  9601  cantnfp1lem3  9609  cantnflem4  9621  tcrank  9813  updjudhcoinlf  9861  updjudhcoinrg  9862  updjud  9863  infpwfien  9991  cardinfima  10026  dfacacn  10071  cfflb  10188  cofsmo  10198  cfcoflem  10201  coftr  10202  fin23lem40  10280  axdc3lem2  10380  ac6num  10408  ac6c4  10410  ac6s2  10415  ttukeylem6  10443  iunfo  10468  pwcfsdom  10512  fpwwe2lem5  10564  fpwwe2lem7  10566  pwfseqlem3  10589  inar1  10704  tskcard  10710  tskuni  10712  tskurn  10718  gruima  10731  nqerrel  10861  recmulnq  10893  dmrecnq  10897  axpre-sup  11098  ofsubeq0  12159  dfz2  12524  uzn0  12786  rpnnen1lem3  12914  rpnnen1lem5  12916  unirnioo  13386  dfioo2  13387  ioorebas  13388  fseq1p1m1  13535  2ffzeq  13586  fvinim0ffz  13723  injresinjlem  13724  fsequb2  13917  fseqsupcl  13918  fseqsupubi  13919  ser0f  13996  hashgval  14274  hashinf  14276  hashresfn  14281  ffz0hash  14388  fnfzo0hash  14391  wrdred1hash  14502  revlen  14703  revrev  14708  repswlen  14717  repsdf2  14719  cshword  14732  0csh0  14734  lenco  14774  s1co  14775  cshco  14778  swrdco  14779  s7f1o  14908  ofccat  14911  shftf  15021  uzin2  15287  rexanuz  15288  limsuple  15420  limsupval2  15422  rlimres  15500  lo1res  15501  rlimresb  15507  isercolllem2  15608  isercolllem3  15609  isercoll  15610  supcvg  15798  prodf1f  15834  eff2  16043  reeff1  16064  tanval  16072  ruclem4  16178  ruclem12  16185  prmreclem6  16868  1arithlem4  16873  1arith  16874  vdwmc  16925  vdwlem1  16928  vdwlem8  16935  vdwlem13  16940  ramval  16955  0ram  16967  0ram2  16968  0ramcl  16970  ramcl  16976  fsets  17115  firest  17371  0ssc  17775  0subcat  17776  isfull2  17851  arwhoma  17983  gsumval2a  18588  isgrpinv  18901  kerf1ghm  19155  f1omvdconj  19352  pmtrmvd  19362  pmtrfinv  19367  pmtrdifellem4  19385  efgsfo  19645  efgredlem  19653  efgcpbllemb  19661  frgpup3lem  19683  0frgp  19685  gexex  19759  torsubg  19760  gsumval3  19813  gsumzres  19815  gsummptmhm  19846  gsumzoppg  19850  dprdf1o  19940  dprd2db  19951  zrinitorngc  20527  zrtermorngc  20528  zrtermoringc  20560  srngf1o  20733  lmhmima  20930  lmhmpreima  20931  lmhmrnlss  20933  lspextmo  20939  pwssplit1  20942  cnfldadd  21246  cnfldmul  21248  dfcnfldOLD  21256  cnfldplusf  21284  cnfldsub  21285  chrrhm  21417  znunit  21449  psgnevpmb  21472  psgndiflemB  21485  mpofrlmd  21662  frlmipval  21664  frlmphl  21666  frlmlbs  21682  frlmup4  21686  ellspd  21687  lindfmm  21712  lsslindf  21715  psrbaglefi  21811  psrlidm  21847  mplmonmul  21919  evlseu  21966  mpfconst  21984  mpfproj  21985  mpfsubrg  21986  coe1sclmulfv  22145  pf1const  22209  pf1id  22210  pf1subrg  22211  mpfpf1  22214  pf1mpf  22215  mamuass  22265  mamudi  22266  mamudir  22267  mamuvs1  22268  mamuvs2  22269  1mavmul  22411  mavmulass  22412  mdetunilem7  22481  madutpos  22505  lecldbas  23082  lmbr2  23122  cncnpi  23141  cncnp  23143  cnpdis  23156  lmff  23164  pnrmopn  23206  dnsconst  23241  cmpsub  23263  tgcmp  23264  hauscmplem  23269  2ndcctbss  23318  2ndcomap  23321  2ndcsep  23322  1stccnp  23325  kgenidm  23410  iskgen2  23411  1stckgen  23417  kgen2cn  23422  ptpjpre1  23434  pttop  23445  ptuni  23457  ptval2  23464  tx1cn  23472  tx2cn  23473  ptpjcn  23474  ptpjopn  23475  ptclsg  23478  ptcnplem  23484  upxp  23486  txcnmpt  23487  uptx  23488  txcmplem2  23505  txkgen  23515  xkoptsub  23517  xkopt  23518  xkococnlem  23522  xkococn  23523  ptcmpfi  23676  zfbas  23759  uzrest  23760  rnelfmlem  23815  rnelfm  23816  fmfnfmlem2  23818  fmfnfm  23821  lmflf  23868  alexsubALT  23914  clssubg  23972  qustgplem  23984  tsmsres  24007  tsmsxplem1  24016  ucncn  24148  xmettpos  24213  imasdsf1olem  24237  blrnps  24272  blrn  24273  xmeterval  24296  tmslem  24346  tmsxms  24350  imasf1oxms  24353  prdsxms  24394  blval2  24426  metuel2  24429  isngp2  24461  isngp3  24462  tngngp2  24516  isnghm  24587  qtopbaslem  24622  qdensere  24633  cnbl0  24637  cnblcld  24638  cnfldms  24639  blssioo  24659  tgioo  24660  tgqioo  24664  xrtgioo  24671  xrsdsre  24675  xrge0tsms  24699  iimulcnOLD  24811  bndth  24833  lebnumlem3  24838  nmhmcn  24996  cphsqrtcl  25060  lmmbr2  25135  caucfil  25159  causs  25174  lmcau  25189  bcth3  25207  cncms  25231  cnfldcusp  25233  rrxmvallem  25280  ivthicc  25335  ovolfioo  25344  ovolficc  25345  ovolficcss  25346  ovollb2lem  25365  ovoliunlem2  25380  ovolshftlem1  25386  ovolicc2  25399  ismbl  25403  voliunlem2  25428  volsup  25433  ioorf  25450  ioorinv  25453  ioorcl  25454  uniiccdif  25455  uniioovol  25456  uniiccvol  25457  uniioombllem2  25460  uniioombllem4  25463  dyaddisj  25473  dyadmax  25475  dyadmbllem  25476  dyadmbl  25477  opnmbllem  25478  opnmblALT  25480  volsup2  25482  mbfdm  25503  mbfima  25507  mbfid  25512  ismbfd  25516  mbfres2  25522  mbfposr  25529  mbfimaopnlem  25532  mbflimsup  25543  0plef  25549  i1f1lem  25566  itg11  25568  itg1addlem4  25576  i1fpos  25583  itg1le  25590  itg1climres  25591  mbfi1fseqlem5  25596  mbfi1flimlem  25599  xrge0f  25608  itg2ge0  25612  itg2seq  25619  itg2i1fseqle  25631  itg2i1fseq2  25633  itg2addlem  25635  itg2gt0  25637  limciun  25771  dvres  25788  dvres3a  25791  cpnres  25815  dvfre  25831  dvmptres3  25836  dvlip2  25876  dvgt0lem2  25884  deg1fvi  25966  uc1pmon1p  26033  fta1g  26051  ig1peu  26056  ig1pdvds  26061  plyco0  26073  plypf1  26093  dgrlem  26110  dgrub  26115  dgrlb  26117  coemulc  26136  plyreres  26166  plydivlem3  26179  plydivlem4  26180  plydiveu  26182  plyremlem  26188  fta1lem  26191  fta1  26192  vieta1lem2  26195  plyexmo  26197  elaa  26200  elqaalem3  26205  aannenlem1  26212  pserulm  26307  psercnlem2  26310  psercnlem1  26311  psercn  26312  abelth  26327  reeff1o  26333  pilem1  26337  recosf1o  26420  resinf1o  26421  efif1olem3  26429  efif1olem4  26430  efifo  26432  eff1olem  26433  ellogrn  26444  logcn  26532  dvloglem  26533  logf1o2  26535  efopnlem1  26541  efopnlem2  26542  efopn  26543  logtayl  26545  cxpcn3lem  26633  cxpcn3  26634  resqrtcn  26635  asinneg  26772  areambl  26844  emcllem7  26888  lgamgulm2  26922  basellem4  26970  sqff1o  27068  mpodvdsmulf1o  27080  fsumdvdsmul  27081  dvdsmulf1o  27082  fsumdvdsmulOLD  27083  ostthlem1  27514  ostth  27526  noetasuplem4  27624  madeval2  27737  elold  27757  old1  27763  madeoldsuc  27772  tglnfn  28450  f1otrg  28774  axlowdimlem6  28850  axlowdimlem8  28852  axlowdimlem9  28853  axlowdimlem11  28855  axlowdimlem12  28856  axlowdimlem17  28861  elntg2  28888  dfpth2  29632  cyclnumvtx  29703  crctcshlem4  29723  clwlkclwwlklem2  29902  eucrct2eupth  30147  ex-fpar  30364  cnnvm  30584  sspmlem  30634  nvo00  30663  nmlno0lem  30695  phoeqi  30759  ubthlem1  30772  hhip  31079  hhssabloilem  31163  hhssnv  31166  hhsssh  31171  occllem  31205  shsel  31216  chscllem2  31540  df0op2  31654  hoeq  31662  hocofni  31669  hoaddfni  31672  hosubfni  31673  hon0  31695  ho01i  31730  hoeq1  31732  elnlfn  31830  nmlnop0iALT  31897  lnopco0i  31906  imaelshi  31960  nlelchi  31963  rnbra  32009  cnvbraval  32012  kbass5  32022  hmopidmchi  32053  hmopidmpji  32054  foresf1o  32406  fcomptf  32555  ofpreima  32562  resf1o  32626  maprnin  32627  fpwrelmapffslem  32628  hashgt1  32706  indpi1  32756  indpreima  32761  s3clhash  32842  gsumpart  32970  xrge0tsmsd  32975  tocyc01  33048  cyc3evpm  33080  cycpmgcl  33083  cycpmconjslem2  33085  cyc3conja  33087  kerunit  33270  1arithidomlem1  33479  1arithidomlem2  33480  1arithidom  33481  dimval  33569  dimvalfi  33570  ply1degltdimlem  33591  ply1degltdim  33592  elirng  33654  txomap  33797  locfinreflem  33803  hauseqcn  33861  xpinpreima  33869  xpinpreima2  33870  tpr2rico  33875  mndpluscn  33889  raddcn  33892  xrge0pluscn  33903  xrge0tmdALT  33909  rge0scvg  33912  pl1cn  33918  elzrhunit  33940  qqhf  33949  cnrrext  33973  qqhre  33983  1stmbfm  34224  2ndmbfm  34225  mbfmcnt  34232  omssubadd  34264  carsggect  34282  eulerpartlemsv2  34322  eulerpartlems  34324  eulerpartlemv  34328  eulerpartlemb  34332  eulerpartlemf  34334  eulerpartlemt  34335  eulerpartlemmf  34339  eulerpartlemgvv  34340  eulerpartlemgh  34342  eulerpartlemgs2  34344  sseqmw  34355  sseqf  34356  sseqp1  34359  fiblem  34362  fibp1  34365  plymul02  34510  signsvtn0  34534  signstres  34539  signshlen  34554  reprinrn  34582  circlemethhgt  34607  txsconnlem  35200  iccllysconn  35210  rellysconn  35211  cvmseu  35236  cvmliftmolem2  35242  cvmliftlem6  35250  cvmliftlem7  35251  cvmliftlem8  35252  cvmliftlem9  35253  cvmliftlem11  35255  cvmliftlem15  35258  cvmlift2lem7  35269  cvmlift2lem10  35272  cvmlift3lem8  35286  cvmlift3lem9  35287  mvrsfpw  35466  mrsubff1  35474  msrid  35505  msrfo  35506  elmsta  35508  mtyf  35512  msubff1  35516  vhmcls  35526  mclsax  35529  elmthm  35536  mthmblem  35540  mclsppslem  35543  iprodefisumlem  35700  fullfunfnv  35907  fullfunfv  35908  tailfb  36338  filnetlem4  36342  taupilem3  37280  icoreresf  37313  icoreelrnab  37315  relowlssretop  37324  relowlpssretop  37325  unccur  37570  matunitlindflem1  37583  matunitlindflem2  37584  ptrecube  37587  poimirlem28  37615  poimirlem32  37619  heicant  37622  opnmbllem0  37623  mblfinlem1  37624  mblfinlem2  37625  volsupnfl  37632  cnambfre  37635  dvtan  37637  itg2addnclem  37638  itg2addnclem2  37639  ftc1anclem3  37662  ftc1anclem5  37664  ftc1anclem7  37666  ftc1anclem8  37667  ftc1anc  37668  areacirc  37680  indexdom  37701  sdclem2  37709  sstotbnd2  37741  sstotbnd  37742  isbndx  37749  isbnd3b  37752  prdsbnd  37760  prdstotbnd  37761  ismtyhmeolem  37771  heibor1lem  37776  heiborlem1  37778  heibor  37788  rrnequiv  37802  keridl  37999  ellkr  39055  lkr0f  39060  cdleme50rnlem  40511  aks6d1c2lem4  42088  aks6d1c5  42100  sticksstones11  42117  sticksstones19  42126  sticksstones22  42129  aks6d1c6lem4  42134  aks6d1c6isolem2  42136  fsuppind  42551  elrfirn  42656  ismrcd2  42660  isnacs2  42667  nacsfix  42673  mapfzcons1  42678  mzpcompact2lem  42712  eq0rabdioph  42737  eldioph4b  42772  diophren  42774  pw2f1ocnv  42999  pw2f1o2val2  43002  lmhmfgsplit  43048  pwssplit4  43051  hbt  43092  mpaaeu  43112  mendring  43150  proot1mul  43156  proot1hash  43157  proot1ex  43158  deg1mhm  43162  fgraphopab  43165  hausgraph  43167  nvocnvb  43384  ofsubid  44286  expgrowthi  44295  expgrowth  44297  binomcxplemdvbinom  44315  binomcxplemcvg  44316  binomcxplemnotnn0  44318  relpfrlem  44916  rfcnpre1  44986  rfcnpre2  44998  cncmpmax  44999  rfcnpre3  45000  rfcnpre4  45001  elixpconstg  45056  ffi  45140  islptre  45590  resincncf  45846  dvcosre  45883  dvresntr  45889  volioof  45958  stoweidlem48  46019  fourierdlem12  46090  fourierdlem15  46093  fourierdlem41  46119  fourierdlem42  46120  fourierdlem46  46123  fourierdlem48  46125  fourierdlem49  46126  fourierdlem54  46131  fourierdlem56  46133  fourierdlem62  46139  fourierdlem64  46141  fourierdlem65  46142  fourierdlem73  46150  fourierdlem74  46151  fourierdlem75  46152  fourierdlem102  46179  fourierdlem103  46180  fourierdlem104  46181  fourierdlem114  46191  sge0split  46380  elhoi  46513  mbfresmf  46710  cjnpoly  46863  cfsetsnfsetf1  47033  cfsetsnfsetfo  47034  focofob  47054  f1ocof1ob  47055  fafvelcdm  47144  ffnafv  47145  fafv2elcdm  47208  fafv2elrnb  47209  imarnf1pr  47256  2ffzoeq  47301  fundcmpsurbijinjpreimafv  47381  fundcmpsurinjimaid  47385  fargshiftfv  47413  fargshiftf  47414  fargshiftf1  47415  fargshiftfo  47416  cycl3grtri  47919  fdmdifeqresdif  48303  fdivmpt  48502  fdivmptf  48503  refdivmptf  48504  1arymaptf1  48604  2arymaptf1  48615  ackfnnn0  48647  homf0  48971  aacllem  49763