Theorem ffn 6508

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

Syntax hints:   → wi 4   ⊆ wss 3935  ran crn 5550   Fn wfn 6344  ⟶wf 6345

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 399  df-f 6353

This theorem is referenced by:  ffnd  6509  ffun  6511  frel  6513  fdm  6516  ffrn  6520  fresin  6541  fresaun  6543  fresaunres2  6544  fcoi1  6546  feu  6548  f0bi  6556  dffo2  6588  fimadmfo  6593  feqmptdf  6729  fvco3  6754  ffvelrn  6843  dff2  6859  dffo3  6862  dffo4  6863  dffo5  6864  f1ompt  6869  ffnfv  6876  frnssb  6879  fcompt  6889  fsn2  6892  fprb  6950  fconst2g  6959  fpr2g  6968  fex  6983  dff13  7007  nvocnv  7032  soisores  7074  fo1stres  7709  fo2ndres  7710  1stcof  7713  2ndcof  7714  curry1f  7795  curry2f  7797  fparlem1  7801  fparlem2  7802  fo2ndf  7811  tposf2  7910  smo11  7995  mapsnd  8444  pw2f1olem  8615  mapen  8675  mapunen  8680  fissuni  8823  fipreima  8824  indexfi  8826  mapfien  8865  oismo  8998  cantnflt  9129  cantnfp1lem3  9137  cantnflem4  9149  tcrank  9307  updjudhcoinlf  9355  updjudhcoinrg  9356  updjud  9357  infpwfien  9482  cardinfima  9517  dfacacn  9561  cfflb  9675  cofsmo  9685  cfcoflem  9688  coftr  9689  fin23lem40  9767  axdc3lem2  9867  ac6num  9895  ac6c4  9897  ac6s2  9902  ttukeylem6  9930  iunfo  9955  pwcfsdom  9999  fpwwe2lem6  10051  fpwwe2lem8  10053  pwfseqlem3  10076  inar1  10191  tskcard  10197  tskuni  10199  tskurn  10205  gruima  10218  nqerrel  10348  recmulnq  10380  dmrecnq  10384  axpre-sup  10585  ofsubeq0  11629  dfz2  11994  uzn0  12254  rpnnen1lem3  12372  rpnnen1lem5  12374  unirnioo  12831  dfioo2  12832  ioorebas  12833  fseq1p1m1  12975  2ffzeq  13022  fvinim0ffz  13150  injresinjlem  13151  fsequb2  13338  fseqsupcl  13339  fseqsupubi  13340  ser0f  13417  hashgval  13687  hashinf  13689  hashresfn  13694  ffz0hash  13799  fnfzo0hash  13802  wrdred1hash  13907  revlen  14118  revrev  14123  repswlen  14132  repsdf2  14134  cshword  14147  0csh0  14149  lenco  14188  s1co  14189  cshco  14192  swrdco  14193  ofccat  14323  shftf  14432  uzin2  14698  rexanuz  14699  limsuple  14829  limsupval2  14831  rlimres  14909  lo1res  14910  rlimresb  14916  isercolllem2  15016  isercolllem3  15017  isercoll  15018  supcvg  15205  prodf1f  15242  eff2  15446  reeff1  15467  tanval  15475  ruclem4  15581  ruclem12  15588  prmreclem6  16251  1arithlem4  16256  1arith  16257  vdwmc  16308  vdwlem1  16311  vdwlem8  16318  vdwlem13  16323  ramval  16338  0ram  16350  0ram2  16351  0ramcl  16353  ramcl  16359  fsets  16510  firest  16700  0ssc  17101  0subcat  17102  isfull2  17175  arwhoma  17299  gsumval2a  17889  isgrpinv  18150  f1omvdconj  18568  pmtrmvd  18578  pmtrfinv  18583  pmtrdifellem4  18601  efgsfo  18859  efgredlem  18867  efgcpbllemb  18875  frgpup3lem  18897  0frgp  18899  gexex  18967  torsubg  18968  gsumval3  19021  gsumzres  19023  gsummptmhm  19054  gsumzoppg  19058  dprdf1o  19148  dprd2db  19159  kerf1ghm  19491  kerf1hrmOLD  19492  srngf1o  19619  lmhmima  19813  lmhmpreima  19814  lmhmrnlss  19816  lspextmo  19822  pwssplit1  19825  psrbaglefi  20146  psrlidm  20177  mplmonmul  20239  evlseu  20290  mpfconst  20308  mpfproj  20309  mpfsubrg  20310  coe1sclmulfv  20445  pf1const  20503  pf1id  20504  pf1subrg  20505  mpfpf1  20508  pf1mpf  20509  cnfldplusf  20566  cnfldsub  20567  chrrhm  20672  znunit  20704  psgnevpmb  20725  psgndiflemB  20738  mpofrlmd  20915  frlmipval  20917  frlmphl  20919  frlmlbs  20935  frlmup4  20939  ellspd  20940  lindfmm  20965  lsslindf  20968  mamuass  21005  mamudi  21006  mamudir  21007  mamuvs1  21008  mamuvs2  21009  1mavmul  21151  mavmulass  21152  mdetunilem7  21221  madutpos  21245  lecldbas  21821  lmbr2  21861  cncnpi  21880  cncnp  21882  cnpdis  21895  lmff  21903  pnrmopn  21945  dnsconst  21980  cmpsub  22002  tgcmp  22003  hauscmplem  22008  2ndcctbss  22057  2ndcomap  22060  2ndcsep  22061  1stccnp  22064  kgenidm  22149  iskgen2  22150  1stckgen  22156  kgen2cn  22161  ptpjpre1  22173  pttop  22184  ptuni  22196  ptval2  22203  tx1cn  22211  tx2cn  22212  ptpjcn  22213  ptpjopn  22214  ptclsg  22217  ptcnplem  22223  upxp  22225  txcnmpt  22226  uptx  22227  txcmplem2  22244  txkgen  22254  xkoptsub  22256  xkopt  22257  xkococnlem  22261  xkococn  22262  ptcmpfi  22415  zfbas  22498  uzrest  22499  rnelfmlem  22554  rnelfm  22555  fmfnfmlem2  22557  fmfnfm  22560  lmflf  22607  alexsubALT  22653  clssubg  22711  qustgplem  22723  tsmsres  22746  tsmsxplem1  22755  ucncn  22888  xmettpos  22953  imasdsf1olem  22977  blrnps  23012  blrn  23013  xmeterval  23036  tmslem  23086  tmsxms  23090  imasf1oxms  23093  prdsxms  23134  blval2  23166  metuel2  23169  isngp2  23200  isngp3  23201  tngngp2  23255  isnghm  23326  qtopbaslem  23361  qdensere  23372  cnbl0  23376  cnblcld  23377  cnfldms  23378  blssioo  23397  tgioo  23398  tgqioo  23402  xrtgioo  23408  xrsdsre  23412  xrge0tsms  23436  iimulcn  23536  bndth  23556  lebnumlem3  23561  nmhmcn  23718  cphsqrtcl  23782  lmmbr2  23856  caucfil  23880  causs  23895  lmcau  23910  bcth3  23928  cncms  23952  cnfldcusp  23954  rrxmvallem  24001  ivthicc  24053  ovolfioo  24062  ovolficc  24063  ovolficcss  24064  ovollb2lem  24083  ovoliunlem2  24098  ovolshftlem1  24104  ovolicc2  24117  ismbl  24121  voliunlem2  24146  volsup  24151  ioorf  24168  ioorinv  24171  ioorcl  24172  uniiccdif  24173  uniioovol  24174  uniiccvol  24175  uniioombllem2  24178  uniioombllem4  24181  dyaddisj  24191  dyadmax  24193  dyadmbllem  24194  dyadmbl  24195  opnmbllem  24196  opnmblALT  24198  volsup2  24200  mbfdm  24221  mbfima  24225  mbfid  24230  ismbfd  24234  mbfres2  24240  mbfposr  24247  mbfimaopnlem  24250  mbflimsup  24261  0plef  24267  i1f1lem  24284  itg11  24286  itg1addlem4  24294  i1fpos  24301  itg1le  24308  itg1climres  24309  mbfi1fseqlem5  24314  mbfi1flimlem  24317  xrge0f  24326  itg2ge0  24330  itg2seq  24337  itg2i1fseqle  24349  itg2i1fseq2  24351  itg2addlem  24353  itg2gt0  24355  limciun  24486  dvres  24503  dvres3a  24506  cpnres  24528  dvfre  24542  dvmptres3  24547  dvlip2  24586  dvgt0lem2  24594  deg1fvi  24673  uc1pmon1p  24739  fta1g  24755  ig1peu  24759  ig1pdvds  24764  plyco0  24776  plypf1  24796  dgrlem  24813  dgrub  24818  dgrlb  24820  coemulc  24839  plyreres  24866  plydivlem3  24878  plydivlem4  24879  plydiveu  24881  plyremlem  24887  fta1lem  24890  fta1  24891  vieta1lem2  24894  plyexmo  24896  elaa  24899  elqaalem3  24904  aannenlem1  24911  pserulm  25004  psercnlem2  25006  psercnlem1  25007  psercn  25008  abelth  25023  reeff1o  25029  pilem1  25033  recosf1o  25113  resinf1o  25114  efif1olem3  25122  efif1olem4  25123  efifo  25125  eff1olem  25126  ellogrn  25137  logcn  25224  dvloglem  25225  logf1o2  25227  efopnlem1  25233  efopnlem2  25234  efopn  25235  logtayl  25237  cxpcn3lem  25322  cxpcn3  25323  resqrtcn  25324  asinneg  25458  areambl  25530  emcllem7  25573  lgamgulm2  25607  basellem4  25655  sqff1o  25753  dvdsmulf1o  25765  fsumdvdsmul  25766  ostthlem1  26197  ostth  26209  tglnfn  26327  f1otrg  26651  axlowdimlem6  26727  axlowdimlem8  26729  axlowdimlem9  26730  axlowdimlem11  26732  axlowdimlem12  26733  axlowdimlem17  26738  elntg2  26765  crctcshlem4  27592  clwlkclwwlklem2  27772  eucrct2eupth  28018  ex-fpar  28235  cnnvm  28453  sspmlem  28503  nvo00  28532  nmlno0lem  28564  phoeqi  28628  ubthlem1  28641  hhip  28948  hhssabloilem  29032  hhssnv  29035  hhsssh  29040  occllem  29074  shsel  29085  chscllem2  29409  df0op2  29523  hoeq  29531  hocofni  29538  hoaddfni  29541  hosubfni  29542  hon0  29564  ho01i  29599  hoeq1  29601  elnlfn  29699  nmlnop0iALT  29766  lnopco0i  29775  imaelshi  29829  nlelchi  29832  rnbra  29878  cnvbraval  29881  kbass5  29891  hmopidmchi  29922  hmopidmpji  29923  foresf1o  30259  fimarab  30384  fcomptf  30397  ofpreima  30404  resf1o  30460  maprnin  30461  fpwrelmapffslem  30462  hashgt1  30524  s3clhash  30619  xrge0tsmsd  30687  tocyc01  30755  cyc3evpm  30787  cycpmgcl  30790  cycpmconjslem2  30792  cyc3conja  30794  kerunit  30891  dimval  30996  dimvalfi  30997  txomap  31093  locfinreflem  31099  hauseqcn  31133  xpinpreima  31144  xpinpreima2  31145  tpr2rico  31150  mndpluscn  31164  rmulccn  31166  raddcn  31167  xrge0pluscn  31178  xrge0tmdALT  31184  rge0scvg  31187  pl1cn  31193  elzrhunit  31215  qqhf  31222  cnrrext  31246  qqhre  31256  indpi1  31274  indpreima  31279  1stmbfm  31513  2ndmbfm  31514  mbfmcnt  31521  omssubadd  31553  carsggect  31571  eulerpartlemsv2  31611  eulerpartlems  31613  eulerpartlemv  31617  eulerpartlemb  31621  eulerpartlemf  31623  eulerpartlemt  31624  eulerpartlemmf  31628  eulerpartlemgvv  31629  eulerpartlemgh  31631  eulerpartlemgs2  31633  sseqmw  31644  sseqf  31645  sseqp1  31648  fiblem  31651  fibp1  31654  plymul02  31811  signsvtn0  31835  signstres  31840  signshlen  31855  reprinrn  31884  circlemethhgt  31909  txsconnlem  32482  iccllysconn  32492  rellysconn  32493  cvmseu  32518  cvmliftmolem2  32524  cvmliftlem6  32532  cvmliftlem7  32533  cvmliftlem8  32534  cvmliftlem9  32535  cvmliftlem11  32537  cvmliftlem15  32540  cvmlift2lem7  32551  cvmlift2lem10  32554  cvmlift3lem8  32568  cvmlift3lem9  32569  mvrsfpw  32748  mrsubff1  32756  msrid  32787  msrfo  32788  elmsta  32790  mtyf  32794  msubff1  32798  vhmcls  32808  mclsax  32811  elmthm  32818  mthmblem  32822  mclsppslem  32825  iprodefisumlem  32967  soseq  33091  noetalem3  33214  madeval2  33285  fullfunfnv  33402  fullfunfv  33403  tailfb  33720  filnetlem4  33724  taupilem3  34594  icoreresf  34627  icoreelrnab  34629  relowlssretop  34638  relowlpssretop  34639  unccur  34869  matunitlindflem1  34882  matunitlindflem2  34883  ptrecube  34886  poimirlem28  34914  poimirlem32  34918  heicant  34921  opnmbllem0  34922  mblfinlem1  34923  mblfinlem2  34924  volsupnfl  34931  cnambfre  34934  dvtan  34936  itg2addnclem  34937  itg2addnclem2  34938  ftc1anclem3  34963  ftc1anclem5  34965  ftc1anclem7  34967  ftc1anclem8  34968  ftc1anc  34969  areacirc  34981  indexdom  35003  sdclem2  35011  sstotbnd2  35046  sstotbnd  35047  isbndx  35054  isbnd3b  35057  prdsbnd  35065  prdstotbnd  35066  ismtyhmeolem  35076  heibor1lem  35081  heiborlem1  35083  heibor  35093  rrnequiv  35107  keridl  35304  ellkr  36219  lkr0f  36224  cdleme50rnlem  37674  elrfirn  39285  ismrcd2  39289  isnacs2  39296  nacsfix  39302  mapfzcons1  39307  mzpcompact2lem  39341  eq0rabdioph  39366  eldioph4b  39401  diophren  39403  pw2f1ocnv  39627  pw2f1o2val2  39630  lmhmfgsplit  39679  pwssplit4  39682  hbt  39723  mpaaeu  39743  mendring  39785  proot1mul  39792  proot1hash  39793  proot1ex  39794  deg1mhm  39800  fgraphopab  39803  hausgraph  39805  ofsubid  40649  expgrowthi  40658  expgrowth  40660  binomcxplemdvbinom  40678  binomcxplemcvg  40679  binomcxplemnotnn0  40681  rfcnpre1  41269  rfcnpre2  41281  cncmpmax  41282  rfcnpre3  41283  rfcnpre4  41284  elixpconstg  41348  ffi  41422  dffo3f  41431  islptre  41893  resincncf  42151  dvcosre  42189  dvresntr  42195  volioof  42266  stoweidlem48  42327  fourierdlem12  42398  fourierdlem15  42401  fourierdlem41  42427  fourierdlem42  42428  fourierdlem46  42431  fourierdlem48  42433  fourierdlem49  42434  fourierdlem54  42439  fourierdlem56  42441  fourierdlem62  42447  fourierdlem64  42449  fourierdlem65  42450  fourierdlem73  42458  fourierdlem74  42459  fourierdlem75  42460  fourierdlem102  42487  fourierdlem103  42488  fourierdlem104  42489  fourierdlem114  42499  sge0split  42685  elhoi  42818  mbfresmf  43010  fafvelrn  43363  ffnafv  43364  fafv2elrn  43427  fafv2elrnb  43428  imarnf1pr  43475  2ffzoeq  43522  fundcmpsurbijinjpreimafv  43561  fundcmpsurinjimaid  43565  fargshiftfv  43593  fargshiftf  43594  fargshiftf1  43595  fargshiftfo  43596  zrinitorngc  44265  zrtermorngc  44266  zrtermoringc  44335  fdmdifeqresdif  44384  fdivmpt  44594  fdivmptf  44595  refdivmptf  44596  aacllem  44896