Theorem ffn 6691

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

Syntax hints:   → wi 4   ⊆ wss 3917  ran crn 5642   Fn wfn 6509  ⟶wf 6510

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 6518

This theorem is referenced by:  ffnd  6692  ffun  6694  frel  6696  fdm  6700  ffrn  6704  fresin  6732  fresaun  6734  fresaunres2  6735  fcoi1  6737  feu  6739  f0bi  6746  dffo2  6779  fimadmfo  6784  fdmeu  6920  feqmptdf  6934  fimarab  6938  fvco3  6963  ffvelcdm  7056  dff2  7074  dffo3  7077  dffo4  7078  dffo5  7079  dffo3f  7081  f1ompt  7086  ffnfv  7094  fcdmssb  7097  fcompt  7108  fsn2  7111  fprb  7171  fconst2g  7180  fpr2g  7188  fex  7203  dff13  7232  nvocnv  7259  soisores  7305  fdmexb  7886  resf1extb  7913  fo1stres  7997  fo2ndres  7998  1stcof  8001  2ndcof  8002  curry1f  8088  curry2f  8090  fparlem1  8094  fparlem2  8095  fo2ndf  8103  soseq  8141  tposf2  8232  smo11  8336  fsetexb  8840  mapsnd  8862  pw2f1olem  9050  mapen  9111  mapunen  9116  fissuni  9315  fipreima  9316  indexfi  9318  mapfien  9366  oismo  9500  cantnflt  9632  cantnfp1lem3  9640  cantnflem4  9652  tcrank  9844  updjudhcoinlf  9892  updjudhcoinrg  9893  updjud  9894  infpwfien  10022  cardinfima  10057  dfacacn  10102  cfflb  10219  cofsmo  10229  cfcoflem  10232  coftr  10233  fin23lem40  10311  axdc3lem2  10411  ac6num  10439  ac6c4  10441  ac6s2  10446  ttukeylem6  10474  iunfo  10499  pwcfsdom  10543  fpwwe2lem5  10595  fpwwe2lem7  10597  pwfseqlem3  10620  inar1  10735  tskcard  10741  tskuni  10743  tskurn  10749  gruima  10762  nqerrel  10892  recmulnq  10924  dmrecnq  10928  axpre-sup  11129  ofsubeq0  12190  dfz2  12555  uzn0  12817  rpnnen1lem3  12945  rpnnen1lem5  12947  unirnioo  13417  dfioo2  13418  ioorebas  13419  fseq1p1m1  13566  2ffzeq  13617  fvinim0ffz  13754  injresinjlem  13755  fsequb2  13948  fseqsupcl  13949  fseqsupubi  13950  ser0f  14027  hashgval  14305  hashinf  14307  hashresfn  14312  ffz0hash  14419  fnfzo0hash  14422  wrdred1hash  14533  revlen  14734  revrev  14739  repswlen  14748  repsdf2  14750  cshword  14763  0csh0  14765  lenco  14805  s1co  14806  cshco  14809  swrdco  14810  s7f1o  14939  ofccat  14942  shftf  15052  uzin2  15318  rexanuz  15319  limsuple  15451  limsupval2  15453  rlimres  15531  lo1res  15532  rlimresb  15538  isercolllem2  15639  isercolllem3  15640  isercoll  15641  supcvg  15829  prodf1f  15865  eff2  16074  reeff1  16095  tanval  16103  ruclem4  16209  ruclem12  16216  prmreclem6  16899  1arithlem4  16904  1arith  16905  vdwmc  16956  vdwlem1  16959  vdwlem8  16966  vdwlem13  16971  ramval  16986  0ram  16998  0ram2  16999  0ramcl  17001  ramcl  17007  fsets  17146  firest  17402  0ssc  17806  0subcat  17807  isfull2  17882  arwhoma  18014  gsumval2a  18619  isgrpinv  18932  kerf1ghm  19186  f1omvdconj  19383  pmtrmvd  19393  pmtrfinv  19398  pmtrdifellem4  19416  efgsfo  19676  efgredlem  19684  efgcpbllemb  19692  frgpup3lem  19714  0frgp  19716  gexex  19790  torsubg  19791  gsumval3  19844  gsumzres  19846  gsummptmhm  19877  gsumzoppg  19881  dprdf1o  19971  dprd2db  19982  zrinitorngc  20558  zrtermorngc  20559  zrtermoringc  20591  srngf1o  20764  lmhmima  20961  lmhmpreima  20962  lmhmrnlss  20964  lspextmo  20970  pwssplit1  20973  cnfldadd  21277  cnfldmul  21279  dfcnfldOLD  21287  cnfldplusf  21315  cnfldsub  21316  chrrhm  21448  znunit  21480  psgnevpmb  21503  psgndiflemB  21516  mpofrlmd  21693  frlmipval  21695  frlmphl  21697  frlmlbs  21713  frlmup4  21717  ellspd  21718  lindfmm  21743  lsslindf  21746  psrbaglefi  21842  psrlidm  21878  mplmonmul  21950  evlseu  21997  mpfconst  22015  mpfproj  22016  mpfsubrg  22017  coe1sclmulfv  22176  pf1const  22240  pf1id  22241  pf1subrg  22242  mpfpf1  22245  pf1mpf  22246  mamuass  22296  mamudi  22297  mamudir  22298  mamuvs1  22299  mamuvs2  22300  1mavmul  22442  mavmulass  22443  mdetunilem7  22512  madutpos  22536  lecldbas  23113  lmbr2  23153  cncnpi  23172  cncnp  23174  cnpdis  23187  lmff  23195  pnrmopn  23237  dnsconst  23272  cmpsub  23294  tgcmp  23295  hauscmplem  23300  2ndcctbss  23349  2ndcomap  23352  2ndcsep  23353  1stccnp  23356  kgenidm  23441  iskgen2  23442  1stckgen  23448  kgen2cn  23453  ptpjpre1  23465  pttop  23476  ptuni  23488  ptval2  23495  tx1cn  23503  tx2cn  23504  ptpjcn  23505  ptpjopn  23506  ptclsg  23509  ptcnplem  23515  upxp  23517  txcnmpt  23518  uptx  23519  txcmplem2  23536  txkgen  23546  xkoptsub  23548  xkopt  23549  xkococnlem  23553  xkococn  23554  ptcmpfi  23707  zfbas  23790  uzrest  23791  rnelfmlem  23846  rnelfm  23847  fmfnfmlem2  23849  fmfnfm  23852  lmflf  23899  alexsubALT  23945  clssubg  24003  qustgplem  24015  tsmsres  24038  tsmsxplem1  24047  ucncn  24179  xmettpos  24244  imasdsf1olem  24268  blrnps  24303  blrn  24304  xmeterval  24327  tmslem  24377  tmsxms  24381  imasf1oxms  24384  prdsxms  24425  blval2  24457  metuel2  24460  isngp2  24492  isngp3  24493  tngngp2  24547  isnghm  24618  qtopbaslem  24653  qdensere  24664  cnbl0  24668  cnblcld  24669  cnfldms  24670  blssioo  24690  tgioo  24691  tgqioo  24695  xrtgioo  24702  xrsdsre  24706  xrge0tsms  24730  iimulcnOLD  24842  bndth  24864  lebnumlem3  24869  nmhmcn  25027  cphsqrtcl  25091  lmmbr2  25166  caucfil  25190  causs  25205  lmcau  25220  bcth3  25238  cncms  25262  cnfldcusp  25264  rrxmvallem  25311  ivthicc  25366  ovolfioo  25375  ovolficc  25376  ovolficcss  25377  ovollb2lem  25396  ovoliunlem2  25411  ovolshftlem1  25417  ovolicc2  25430  ismbl  25434  voliunlem2  25459  volsup  25464  ioorf  25481  ioorinv  25484  ioorcl  25485  uniiccdif  25486  uniioovol  25487  uniiccvol  25488  uniioombllem2  25491  uniioombllem4  25494  dyaddisj  25504  dyadmax  25506  dyadmbllem  25507  dyadmbl  25508  opnmbllem  25509  opnmblALT  25511  volsup2  25513  mbfdm  25534  mbfima  25538  mbfid  25543  ismbfd  25547  mbfres2  25553  mbfposr  25560  mbfimaopnlem  25563  mbflimsup  25574  0plef  25580  i1f1lem  25597  itg11  25599  itg1addlem4  25607  i1fpos  25614  itg1le  25621  itg1climres  25622  mbfi1fseqlem5  25627  mbfi1flimlem  25630  xrge0f  25639  itg2ge0  25643  itg2seq  25650  itg2i1fseqle  25662  itg2i1fseq2  25664  itg2addlem  25666  itg2gt0  25668  limciun  25802  dvres  25819  dvres3a  25822  cpnres  25846  dvfre  25862  dvmptres3  25867  dvlip2  25907  dvgt0lem2  25915  deg1fvi  25997  uc1pmon1p  26064  fta1g  26082  ig1peu  26087  ig1pdvds  26092  plyco0  26104  plypf1  26124  dgrlem  26141  dgrub  26146  dgrlb  26148  coemulc  26167  plyreres  26197  plydivlem3  26210  plydivlem4  26211  plydiveu  26213  plyremlem  26219  fta1lem  26222  fta1  26223  vieta1lem2  26226  plyexmo  26228  elaa  26231  elqaalem3  26236  aannenlem1  26243  pserulm  26338  psercnlem2  26341  psercnlem1  26342  psercn  26343  abelth  26358  reeff1o  26364  pilem1  26368  recosf1o  26451  resinf1o  26452  efif1olem3  26460  efif1olem4  26461  efifo  26463  eff1olem  26464  ellogrn  26475  logcn  26563  dvloglem  26564  logf1o2  26566  efopnlem1  26572  efopnlem2  26573  efopn  26574  logtayl  26576  cxpcn3lem  26664  cxpcn3  26665  resqrtcn  26666  asinneg  26803  areambl  26875  emcllem7  26919  lgamgulm2  26953  basellem4  27001  sqff1o  27099  mpodvdsmulf1o  27111  fsumdvdsmul  27112  dvdsmulf1o  27113  fsumdvdsmulOLD  27114  ostthlem1  27545  ostth  27557  noetasuplem4  27655  madeval2  27768  elold  27788  old1  27794  madeoldsuc  27803  tglnfn  28481  f1otrg  28805  axlowdimlem6  28881  axlowdimlem8  28883  axlowdimlem9  28884  axlowdimlem11  28886  axlowdimlem12  28887  axlowdimlem17  28892  elntg2  28919  dfpth2  29666  cyclnumvtx  29737  crctcshlem4  29757  clwlkclwwlklem2  29936  eucrct2eupth  30181  ex-fpar  30398  cnnvm  30618  sspmlem  30668  nvo00  30697  nmlno0lem  30729  phoeqi  30793  ubthlem1  30806  hhip  31113  hhssabloilem  31197  hhssnv  31200  hhsssh  31205  occllem  31239  shsel  31250  chscllem2  31574  df0op2  31688  hoeq  31696  hocofni  31703  hoaddfni  31706  hosubfni  31707  hon0  31729  ho01i  31764  hoeq1  31766  elnlfn  31864  nmlnop0iALT  31931  lnopco0i  31940  imaelshi  31994  nlelchi  31997  rnbra  32043  cnvbraval  32046  kbass5  32056  hmopidmchi  32087  hmopidmpji  32088  foresf1o  32440  fcomptf  32589  ofpreima  32596  resf1o  32660  maprnin  32661  fpwrelmapffslem  32662  hashgt1  32740  indpi1  32790  indpreima  32795  s3clhash  32876  gsumpart  33004  xrge0tsmsd  33009  tocyc01  33082  cyc3evpm  33114  cycpmgcl  33117  cycpmconjslem2  33119  cyc3conja  33121  kerunit  33304  1arithidomlem1  33513  1arithidomlem2  33514  1arithidom  33515  dimval  33603  dimvalfi  33604  ply1degltdimlem  33625  ply1degltdim  33626  elirng  33688  txomap  33831  locfinreflem  33837  hauseqcn  33895  xpinpreima  33903  xpinpreima2  33904  tpr2rico  33909  mndpluscn  33923  raddcn  33926  xrge0pluscn  33937  xrge0tmdALT  33943  rge0scvg  33946  pl1cn  33952  elzrhunit  33974  qqhf  33983  cnrrext  34007  qqhre  34017  1stmbfm  34258  2ndmbfm  34259  mbfmcnt  34266  omssubadd  34298  carsggect  34316  eulerpartlemsv2  34356  eulerpartlems  34358  eulerpartlemv  34362  eulerpartlemb  34366  eulerpartlemf  34368  eulerpartlemt  34369  eulerpartlemmf  34373  eulerpartlemgvv  34374  eulerpartlemgh  34376  eulerpartlemgs2  34378  sseqmw  34389  sseqf  34390  sseqp1  34393  fiblem  34396  fibp1  34399  plymul02  34544  signsvtn0  34568  signstres  34573  signshlen  34588  reprinrn  34616  circlemethhgt  34641  txsconnlem  35234  iccllysconn  35244  rellysconn  35245  cvmseu  35270  cvmliftmolem2  35276  cvmliftlem6  35284  cvmliftlem7  35285  cvmliftlem8  35286  cvmliftlem9  35287  cvmliftlem11  35289  cvmliftlem15  35292  cvmlift2lem7  35303  cvmlift2lem10  35306  cvmlift3lem8  35320  cvmlift3lem9  35321  mvrsfpw  35500  mrsubff1  35508  msrid  35539  msrfo  35540  elmsta  35542  mtyf  35546  msubff1  35550  vhmcls  35560  mclsax  35563  elmthm  35570  mthmblem  35574  mclsppslem  35577  iprodefisumlem  35734  fullfunfnv  35941  fullfunfv  35942  tailfb  36372  filnetlem4  36376  taupilem3  37314  icoreresf  37347  icoreelrnab  37349  relowlssretop  37358  relowlpssretop  37359  unccur  37604  matunitlindflem1  37617  matunitlindflem2  37618  ptrecube  37621  poimirlem28  37649  poimirlem32  37653  heicant  37656  opnmbllem0  37657  mblfinlem1  37658  mblfinlem2  37659  volsupnfl  37666  cnambfre  37669  dvtan  37671  itg2addnclem  37672  itg2addnclem2  37673  ftc1anclem3  37696  ftc1anclem5  37698  ftc1anclem7  37700  ftc1anclem8  37701  ftc1anc  37702  areacirc  37714  indexdom  37735  sdclem2  37743  sstotbnd2  37775  sstotbnd  37776  isbndx  37783  isbnd3b  37786  prdsbnd  37794  prdstotbnd  37795  ismtyhmeolem  37805  heibor1lem  37810  heiborlem1  37812  heibor  37822  rrnequiv  37836  keridl  38033  ellkr  39089  lkr0f  39094  cdleme50rnlem  40545  aks6d1c2lem4  42122  aks6d1c5  42134  sticksstones11  42151  sticksstones19  42160  sticksstones22  42163  aks6d1c6lem4  42168  aks6d1c6isolem2  42170  fsuppind  42585  elrfirn  42690  ismrcd2  42694  isnacs2  42701  nacsfix  42707  mapfzcons1  42712  mzpcompact2lem  42746  eq0rabdioph  42771  eldioph4b  42806  diophren  42808  pw2f1ocnv  43033  pw2f1o2val2  43036  lmhmfgsplit  43082  pwssplit4  43085  hbt  43126  mpaaeu  43146  mendring  43184  proot1mul  43190  proot1hash  43191  proot1ex  43192  deg1mhm  43196  fgraphopab  43199  hausgraph  43201  nvocnvb  43418  ofsubid  44320  expgrowthi  44329  expgrowth  44331  binomcxplemdvbinom  44349  binomcxplemcvg  44350  binomcxplemnotnn0  44352  relpfrlem  44950  rfcnpre1  45020  rfcnpre2  45032  cncmpmax  45033  rfcnpre3  45034  rfcnpre4  45035  elixpconstg  45090  ffi  45174  islptre  45624  resincncf  45880  dvcosre  45917  dvresntr  45923  volioof  45992  stoweidlem48  46053  fourierdlem12  46124  fourierdlem15  46127  fourierdlem41  46153  fourierdlem42  46154  fourierdlem46  46157  fourierdlem48  46159  fourierdlem49  46160  fourierdlem54  46165  fourierdlem56  46167  fourierdlem62  46173  fourierdlem64  46175  fourierdlem65  46176  fourierdlem73  46184  fourierdlem74  46185  fourierdlem75  46186  fourierdlem102  46213  fourierdlem103  46214  fourierdlem104  46215  fourierdlem114  46225  sge0split  46414  elhoi  46547  mbfresmf  46744  cfsetsnfsetf1  47064  cfsetsnfsetfo  47065  focofob  47085  f1ocof1ob  47086  fafvelcdm  47175  ffnafv  47176  fafv2elcdm  47239  fafv2elrnb  47240  imarnf1pr  47287  2ffzoeq  47332  fundcmpsurbijinjpreimafv  47412  fundcmpsurinjimaid  47416  fargshiftfv  47444  fargshiftf  47445  fargshiftf1  47446  fargshiftfo  47447  cycl3grtri  47950  fdmdifeqresdif  48334  fdivmpt  48533  fdivmptf  48534  refdivmptf  48535  1arymaptf1  48635  2arymaptf1  48646  ackfnnn0  48678  homf0  49002  aacllem  49794