Theorem ffn 6385

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

Syntax hints:   → wi 4   ⊆ wss 3861  ran crn 5447   Fn wfn 6223  ⟶wf 6224

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 208  df-an 397  df-f 6232

This theorem is referenced by:  ffnd  6386  ffun  6388  frel  6390  fdm  6393  ffrn  6397  fresin  6418  fresaun  6420  fresaunres2  6421  fcoi1  6423  feu  6425  f0bi  6433  dffo2  6465  fimadmfo  6470  feqmptdf  6606  fvco3  6630  ffvelrn  6717  dff2  6731  dffo3  6734  dffo4  6735  dffo5  6736  f1ompt  6741  ffnfv  6748  frnssb  6751  fcompt  6761  fsn2  6764  fprb  6826  fconst2g  6835  fpr2g  6843  fex  6858  dff13  6881  nvocnv  6906  soisores  6946  fo1stres  7574  fo2ndres  7575  1stcof  7578  2ndcof  7579  curry1f  7660  curry2f  7662  fparlem1  7666  fparlem2  7667  fo2ndf  7673  tposf2  7770  smo11  7856  mapsnd  8302  pw2f1olem  8471  mapen  8531  mapunen  8536  fissuni  8678  fipreima  8679  indexfi  8681  mapfien  8720  oismo  8853  cantnflt  8984  cantnfp1lem3  8992  cantnflem4  9004  tcrank  9162  updjudhcoinlf  9210  updjudhcoinrg  9211  updjud  9212  infpwfien  9337  cardinfima  9372  dfacacn  9416  cfflb  9530  cofsmo  9540  cfcoflem  9543  coftr  9544  fin23lem40  9622  axdc3lem2  9722  ac6num  9750  ac6c4  9752  ac6s2  9757  ttukeylem6  9785  iunfo  9810  pwcfsdom  9854  fpwwe2lem6  9906  fpwwe2lem8  9908  pwfseqlem3  9931  inar1  10046  tskcard  10052  tskuni  10054  tskurn  10060  gruima  10073  nqerrel  10203  recmulnq  10235  dmrecnq  10239  axpre-sup  10440  ofsubeq0  11485  dfz2  11850  uzn0  12109  rpnnen1lem3  12228  rpnnen1lem5  12230  unirnioo  12687  dfioo2  12688  ioorebas  12689  fseq1p1m1  12831  2ffzeq  12878  fvinim0ffz  13006  injresinjlem  13007  fsequb2  13194  fseqsupcl  13195  fseqsupubi  13196  ser0f  13273  hashgval  13543  hashinf  13545  hashresfn  13550  ffz0hash  13653  fnfzo0hash  13656  wrdred1hash  13759  ccatass  13786  ccatrn  13787  ccatswrd  13866  swrdccat2  13867  ccatpfx  13899  revlen  13960  revccat  13964  revrev  13965  repswlen  13974  repsdf2  13976  cshword  13989  0csh0  13991  lenco  14030  s1co  14031  cshco  14034  swrdco  14035  ofccat  14163  shftf  14272  uzin2  14538  rexanuz  14539  limsuple  14669  limsupval2  14671  rlimres  14749  lo1res  14750  rlimresb  14756  isercolllem2  14856  isercolllem3  14857  isercoll  14858  supcvg  15044  prodf1f  15081  eff2  15285  reeff1  15306  tanval  15314  ruclem4  15420  ruclem12  15427  prmreclem6  16086  1arithlem4  16091  1arith  16092  vdwmc  16143  vdwlem1  16146  vdwlem8  16153  vdwlem13  16158  ramval  16173  0ram  16185  0ram2  16186  0ramcl  16188  ramcl  16194  fsets  16345  firest  16535  0ssc  16936  0subcat  16937  isfull2  17010  arwhoma  17134  gsumval2a  17718  isgrpinv  17913  f1omvdconj  18305  pmtrmvd  18315  pmtrfinv  18320  pmtrdifellem4  18338  efginvrel2  18580  efgsfo  18592  efgredlem  18600  efgcpbllemb  18608  frgpup3lem  18630  0frgp  18632  gexex  18696  torsubg  18697  gsumval3  18748  gsumzres  18750  gsummptmhm  18780  gsumzoppg  18784  dprdf1o  18871  dprd2db  18882  pgpfaclem1  18920  kerf1ghm  19187  kerf1hrmOLD  19188  srngf1o  19315  lmhmima  19509  lmhmpreima  19510  lmhmrnlss  19512  lspextmo  19518  pwssplit1  19521  psrbaglefi  19840  psrlidm  19871  mplmonmul  19932  evlseu  19983  mpfconst  19997  mpfproj  19998  mpfsubrg  19999  coe1sclmulfv  20134  pf1const  20191  pf1id  20192  pf1subrg  20193  mpfpf1  20196  pf1mpf  20197  cnfldplusf  20254  cnfldsub  20255  chrrhm  20360  znunit  20392  psgnevpmb  20413  psgndiflemB  20426  mpofrlmd  20603  frlmipval  20605  frlmphl  20607  frlmlbs  20623  frlmup4  20627  ellspd  20628  lindfmm  20653  lsslindf  20656  mamuass  20695  mamudi  20696  mamudir  20697  mamuvs1  20698  mamuvs2  20699  1mavmul  20841  mavmulass  20842  mdetunilem7  20911  madutpos  20935  lecldbas  21511  lmbr2  21551  cncnpi  21570  cncnp  21572  cnpdis  21585  lmff  21593  pnrmopn  21635  dnsconst  21670  cmpsub  21692  tgcmp  21693  hauscmplem  21698  2ndcctbss  21747  2ndcomap  21750  2ndcsep  21751  1stccnp  21754  kgenidm  21839  iskgen2  21840  1stckgen  21846  kgen2cn  21851  ptpjpre1  21863  pttop  21874  ptuni  21886  ptval2  21893  tx1cn  21901  tx2cn  21902  ptpjcn  21903  ptpjopn  21904  ptclsg  21907  ptcnplem  21913  upxp  21915  txcnmpt  21916  uptx  21917  txcmplem2  21934  txkgen  21944  xkoptsub  21946  xkopt  21947  xkococnlem  21951  xkococn  21952  ptcmpfi  22105  zfbas  22188  uzrest  22189  rnelfmlem  22244  rnelfm  22245  fmfnfmlem2  22247  fmfnfm  22250  lmflf  22297  alexsubALT  22343  clssubg  22400  qustgplem  22412  tsmsres  22435  tsmsxplem1  22444  ucncn  22577  xmettpos  22642  imasdsf1olem  22666  blrnps  22701  blrn  22702  xmeterval  22725  tmslem  22775  tmsxms  22779  imasf1oxms  22782  prdsxms  22823  blval2  22855  metuel2  22858  isngp2  22889  isngp3  22890  tngngp2  22944  isnghm  23015  qtopbaslem  23050  qdensere  23061  cnbl0  23065  cnblcld  23066  cnfldms  23067  blssioo  23086  tgioo  23087  tgqioo  23091  xrtgioo  23097  xrsdsre  23101  xrge0tsms  23125  iimulcn  23225  bndth  23245  lebnumlem3  23250  nmhmcn  23407  cphsqrtcl  23471  lmmbr2  23545  caucfil  23569  causs  23584  lmcau  23599  bcth3  23617  cncms  23641  cnfldcusp  23643  rrxmvallem  23690  ivthicc  23742  ovolfioo  23751  ovolficc  23752  ovolficcss  23753  ovollb2lem  23772  ovoliunlem2  23787  ovolshftlem1  23793  ovolicc2  23806  ismbl  23810  voliunlem2  23835  volsup  23840  ioorf  23857  ioorinv  23860  ioorcl  23861  uniiccdif  23862  uniioovol  23863  uniiccvol  23864  uniioombllem2  23867  uniioombllem4  23870  dyaddisj  23880  dyadmax  23882  dyadmbllem  23883  dyadmbl  23884  opnmbllem  23885  opnmblALT  23887  volsup2  23889  mbfdm  23910  mbfima  23914  mbfid  23919  ismbfd  23923  mbfres2  23929  mbfposr  23936  mbfimaopnlem  23939  mbflimsup  23950  0plef  23956  i1f1lem  23973  itg11  23975  itg1addlem4  23983  i1fpos  23990  itg1le  23997  itg1climres  23998  mbfi1fseqlem5  24003  mbfi1flimlem  24006  xrge0f  24015  itg2ge0  24019  itg2seq  24026  itg2i1fseqle  24038  itg2i1fseq2  24040  itg2addlem  24042  itg2gt0  24044  limciun  24175  dvres  24192  dvres3a  24195  cpnres  24217  dvfre  24231  dvmptres3  24236  dvlip2  24275  dvgt0lem2  24283  deg1fvi  24362  uc1pmon1p  24428  fta1g  24444  ig1peu  24448  ig1pdvds  24453  plyco0  24465  plypf1  24485  dgrlem  24502  dgrub  24507  dgrlb  24509  coemulc  24528  plyreres  24555  plydivlem3  24567  plydivlem4  24568  plydiveu  24570  plyremlem  24576  fta1lem  24579  fta1  24580  vieta1lem2  24583  plyexmo  24585  elaa  24588  elqaalem3  24593  aannenlem1  24600  pserulm  24693  psercnlem2  24695  psercnlem1  24696  psercn  24697  abelth  24712  reeff1o  24718  pilem1  24722  recosf1o  24800  resinf1o  24801  efif1olem3  24809  efif1olem4  24810  efifo  24812  eff1olem  24813  ellogrn  24824  logcn  24911  dvloglem  24912  logf1o2  24914  efopnlem1  24920  efopnlem2  24921  efopn  24922  logtayl  24924  cxpcn3lem  25009  cxpcn3  25010  resqrtcn  25011  asinneg  25145  areambl  25218  emcllem7  25261  lgamgulm2  25295  basellem4  25343  sqff1o  25441  dvdsmulf1o  25453  fsumdvdsmul  25454  ostthlem1  25885  ostth  25897  tglnfn  26015  f1otrg  26340  axlowdimlem6  26416  axlowdimlem8  26418  axlowdimlem9  26419  axlowdimlem11  26421  axlowdimlem12  26422  axlowdimlem17  26427  elntg2  26454  crctcshlem4  27280  clwlkclwwlklem2  27460  eucrct2eupth  27706  cnnvm  28142  sspmlem  28192  nvo00  28221  nmlno0lem  28253  phoeqi  28317  ubthlem1  28330  hhip  28637  hhssabloilem  28721  hhssnv  28724  hhsssh  28729  occllem  28763  shsel  28774  chscllem2  29098  df0op2  29212  hoeq  29220  hocofni  29227  hoaddfni  29230  hosubfni  29231  hon0  29253  ho01i  29288  hoeq1  29290  elnlfn  29388  nmlnop0iALT  29455  lnopco0i  29464  imaelshi  29518  nlelchi  29521  rnbra  29567  cnvbraval  29570  kbass5  29580  hmopidmchi  29611  hmopidmpji  29612  foresf1o  29949  fimarab  30072  fcomptf  30085  ofpreima  30092  resf1o  30146  maprnin  30147  fpwrelmapffslem  30148  hashgt1  30206  s3clhash  30296  tocyc01  30399  cyc3evpm  30422  cycpmgcl  30425  cycpmconjslem2  30427  cyc3conja  30429  xrge0tsmsd  30495  kerunit  30542  dimval  30597  dimvalfi  30598  txomap  30707  locfinreflem  30713  hauseqcn  30747  xpinpreima  30758  xpinpreima2  30759  tpr2rico  30764  mndpluscn  30778  rmulccn  30780  raddcn  30781  xrge0pluscn  30792  xrge0tmdALT  30798  rge0scvg  30801  pl1cn  30807  elzrhunit  30829  qqhf  30836  cnrrext  30860  qqhre  30870  indpi1  30888  indpreima  30893  1stmbfm  31127  2ndmbfm  31128  mbfmcnt  31135  omssubadd  31167  carsggect  31185  eulerpartlemsv2  31225  eulerpartlems  31227  eulerpartlemv  31231  eulerpartlemb  31235  eulerpartlemf  31237  eulerpartlemt  31238  eulerpartlemmf  31242  eulerpartlemgvv  31243  eulerpartlemgh  31245  eulerpartlemgs2  31247  sseqmw  31258  sseqf  31259  sseqp1  31262  fiblem  31265  fibp1  31268  plymul02  31425  signsvtn0  31449  signstres  31454  signshlen  31469  reprinrn  31498  circlemethhgt  31523  txsconnlem  32089  iccllysconn  32099  rellysconn  32100  cvmseu  32125  cvmliftmolem2  32131  cvmliftlem6  32139  cvmliftlem7  32140  cvmliftlem8  32141  cvmliftlem9  32142  cvmliftlem11  32144  cvmliftlem15  32147  cvmlift2lem7  32158  cvmlift2lem10  32161  cvmlift3lem8  32175  cvmlift3lem9  32176  mvrsfpw  32355  mrsubff1  32363  msrid  32394  msrfo  32395  elmsta  32397  mtyf  32401  msubff1  32405  vhmcls  32415  mclsax  32418  elmthm  32425  mthmblem  32429  mclsppslem  32432  iprodefisumlem  32574  soseq  32699  noetalem3  32822  madeval2  32893  fullfunfnv  33010  fullfunfv  33011  tailfb  33328  filnetlem4  33332  taupilem3  34144  icoreresf  34177  icoreelrnab  34179  relowlssretop  34188  relowlpssretop  34189  unccur  34419  matunitlindflem1  34432  matunitlindflem2  34433  ptrecube  34436  poimirlem28  34464  poimirlem32  34468  heicant  34471  opnmbllem0  34472  mblfinlem1  34473  mblfinlem2  34474  volsupnfl  34481  cnambfre  34484  dvtan  34486  itg2addnclem  34487  itg2addnclem2  34488  ftc1anclem3  34513  ftc1anclem5  34515  ftc1anclem7  34517  ftc1anclem8  34518  ftc1anc  34519  areacirc  34531  indexdom  34554  sdclem2  34562  sstotbnd2  34597  sstotbnd  34598  isbndx  34605  isbnd3b  34608  prdsbnd  34616  prdstotbnd  34617  ismtyhmeolem  34627  heibor1lem  34632  heiborlem1  34634  heibor  34644  rrnequiv  34658  keridl  34855  ellkr  35769  lkr0f  35774  cdleme50rnlem  37224  elrfirn  38790  ismrcd2  38794  isnacs2  38801  nacsfix  38807  mapfzcons1  38812  mzpcompact2lem  38846  eq0rabdioph  38871  eldioph4b  38906  diophren  38908  pw2f1ocnv  39132  pw2f1o2val2  39135  lmhmfgsplit  39184  pwssplit4  39187  hbt  39228  mpaaeu  39248  mendring  39290  proot1mul  39297  proot1hash  39298  proot1ex  39299  deg1mhm  39305  fgraphopab  39308  hausgraph  39310  ofsubid  40207  expgrowthi  40216  expgrowth  40218  binomcxplemdvbinom  40236  binomcxplemcvg  40237  binomcxplemnotnn0  40239  rfcnpre1  40828  rfcnpre2  40840  cncmpmax  40841  rfcnpre3  40842  rfcnpre4  40843  elixpconstg  40907  ffi  40982  dffo3f  40991  islptre  41455  resincncf  41713  dvcosre  41751  dvresntr  41757  volioof  41828  stoweidlem48  41889  fourierdlem12  41960  fourierdlem15  41963  fourierdlem41  41989  fourierdlem42  41990  fourierdlem46  41993  fourierdlem48  41995  fourierdlem49  41996  fourierdlem54  42001  fourierdlem56  42003  fourierdlem62  42009  fourierdlem64  42011  fourierdlem65  42012  fourierdlem73  42020  fourierdlem74  42021  fourierdlem75  42022  fourierdlem102  42049  fourierdlem103  42050  fourierdlem104  42051  fourierdlem114  42061  sge0split  42247  elhoi  42380  mbfresmf  42572  fafvelrn  42899  ffnafv  42900  fafv2elrn  42963  fafv2elrnb  42964  imarnf1pr  43011  2ffzoeq  43058  fargshiftfv  43095  fargshiftf  43096  fargshiftf1  43097  fargshiftfo  43098  zrinitorngc  43763  zrtermorngc  43764  zrtermoringc  43833  fdmdifeqresdif  43882  fdivmpt  44095  fdivmptf  44096  refdivmptf  44097  aacllem  44396