Theorem ffn 6718

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

Syntax hints:   → wi 4   ⊆ wss 3949  ran crn 5678   Fn wfn 6539  ⟶wf 6540

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 206  df-an 395  df-f 6548

This theorem is referenced by:  ffnd  6719  ffun  6721  frel  6723  fdm  6727  fdmOLD  6728  ffrn  6732  fresin  6761  fresaun  6763  fresaunres2  6764  fcoi1  6766  feu  6768  f0bi  6775  dffo2  6810  fimadmfo  6815  feqmptdf  6963  fvco3  6991  ffvelcdm  7084  dff2  7101  dffo3  7104  dffo4  7105  dffo5  7106  dffo3f  7108  f1ompt  7113  ffnfv  7121  fcdmssb  7124  fcompt  7134  fsn2  7137  fprb  7198  fconst2g  7207  fpr2g  7216  fex  7231  dff13  7258  nvocnv  7283  soisores  7328  fdmexb  7904  fo1stres  8005  fo2ndres  8006  1stcof  8009  2ndcof  8010  curry1f  8096  curry2f  8098  fparlem1  8102  fparlem2  8103  fo2ndf  8111  soseq  8149  tposf2  8239  smo11  8368  fsetexb  8862  mapsnd  8884  pw2f1olem  9080  mapen  9145  mapunen  9150  fissuni  9361  fipreima  9362  indexfi  9364  mapfien  9407  oismo  9539  cantnflt  9671  cantnfp1lem3  9679  cantnflem4  9691  tcrank  9883  updjudhcoinlf  9931  updjudhcoinrg  9932  updjud  9933  infpwfien  10061  cardinfima  10096  dfacacn  10140  cfflb  10258  cofsmo  10268  cfcoflem  10271  coftr  10272  fin23lem40  10350  axdc3lem2  10450  ac6num  10478  ac6c4  10480  ac6s2  10485  ttukeylem6  10513  iunfo  10538  pwcfsdom  10582  fpwwe2lem5  10634  fpwwe2lem7  10636  pwfseqlem3  10659  inar1  10774  tskcard  10780  tskuni  10782  tskurn  10788  gruima  10801  nqerrel  10931  recmulnq  10963  dmrecnq  10967  axpre-sup  11168  ofsubeq0  12215  dfz2  12583  uzn0  12845  rpnnen1lem3  12969  rpnnen1lem5  12971  unirnioo  13432  dfioo2  13433  ioorebas  13434  fseq1p1m1  13581  2ffzeq  13628  fvinim0ffz  13757  injresinjlem  13758  fsequb2  13947  fseqsupcl  13948  fseqsupubi  13949  ser0f  14027  hashgval  14299  hashinf  14301  hashresfn  14306  ffz0hash  14412  fnfzo0hash  14415  wrdred1hash  14517  revlen  14718  revrev  14723  repswlen  14732  repsdf2  14734  cshword  14747  0csh0  14749  lenco  14789  s1co  14790  cshco  14793  swrdco  14794  ofccat  14922  shftf  15032  uzin2  15297  rexanuz  15298  limsuple  15428  limsupval2  15430  rlimres  15508  lo1res  15509  rlimresb  15515  isercolllem2  15618  isercolllem3  15619  isercoll  15620  supcvg  15808  prodf1f  15844  eff2  16048  reeff1  16069  tanval  16077  ruclem4  16183  ruclem12  16190  prmreclem6  16860  1arithlem4  16865  1arith  16866  vdwmc  16917  vdwlem1  16920  vdwlem8  16927  vdwlem13  16932  ramval  16947  0ram  16959  0ram2  16960  0ramcl  16962  ramcl  16968  fsets  17108  firest  17384  0ssc  17793  0subcat  17794  isfull2  17868  arwhoma  18001  gsumval2a  18612  isgrpinv  18916  kerf1ghm  19163  f1omvdconj  19357  pmtrmvd  19367  pmtrfinv  19372  pmtrdifellem4  19390  efgsfo  19650  efgredlem  19658  efgcpbllemb  19666  frgpup3lem  19688  0frgp  19690  gexex  19764  torsubg  19765  gsumval3  19818  gsumzres  19820  gsummptmhm  19851  gsumzoppg  19855  dprdf1o  19945  dprd2db  19956  srngf1o  20607  lmhmima  20804  lmhmpreima  20805  lmhmrnlss  20807  lspextmo  20813  pwssplit1  20816  cnfldplusf  21174  cnfldsub  21175  chrrhm  21304  znunit  21340  psgnevpmb  21361  psgndiflemB  21374  mpofrlmd  21553  frlmipval  21555  frlmphl  21557  frlmlbs  21573  frlmup4  21577  ellspd  21578  lindfmm  21603  lsslindf  21606  psrbaglefi  21706  psrbaglefiOLD  21707  psrlidm  21744  mplmonmul  21812  evlseu  21867  mpfconst  21885  mpfproj  21886  mpfsubrg  21887  coe1sclmulfv  22027  pf1const  22087  pf1id  22088  pf1subrg  22089  mpfpf1  22092  pf1mpf  22093  mamuass  22124  mamudi  22125  mamudir  22126  mamuvs1  22127  mamuvs2  22128  1mavmul  22272  mavmulass  22273  mdetunilem7  22342  madutpos  22366  lecldbas  22945  lmbr2  22985  cncnpi  23004  cncnp  23006  cnpdis  23019  lmff  23027  pnrmopn  23069  dnsconst  23104  cmpsub  23126  tgcmp  23127  hauscmplem  23132  2ndcctbss  23181  2ndcomap  23184  2ndcsep  23185  1stccnp  23188  kgenidm  23273  iskgen2  23274  1stckgen  23280  kgen2cn  23285  ptpjpre1  23297  pttop  23308  ptuni  23320  ptval2  23327  tx1cn  23335  tx2cn  23336  ptpjcn  23337  ptpjopn  23338  ptclsg  23341  ptcnplem  23347  upxp  23349  txcnmpt  23350  uptx  23351  txcmplem2  23368  txkgen  23378  xkoptsub  23380  xkopt  23381  xkococnlem  23385  xkococn  23386  ptcmpfi  23539  zfbas  23622  uzrest  23623  rnelfmlem  23678  rnelfm  23679  fmfnfmlem2  23681  fmfnfm  23684  lmflf  23731  alexsubALT  23777  clssubg  23835  qustgplem  23847  tsmsres  23870  tsmsxplem1  23879  ucncn  24012  xmettpos  24077  imasdsf1olem  24101  blrnps  24136  blrn  24137  xmeterval  24160  tmslem  24212  tmslemOLD  24213  tmsxms  24217  imasf1oxms  24220  prdsxms  24261  blval2  24293  metuel2  24296  isngp2  24328  isngp3  24329  tngngp2  24391  isnghm  24462  qtopbaslem  24497  qdensere  24508  cnbl0  24512  cnblcld  24513  cnfldms  24514  blssioo  24533  tgioo  24534  tgqioo  24538  xrtgioo  24544  xrsdsre  24548  xrge0tsms  24572  iimulcnOLD  24684  bndth  24706  lebnumlem3  24711  nmhmcn  24869  cphsqrtcl  24934  lmmbr2  25009  caucfil  25033  causs  25048  lmcau  25063  bcth3  25081  cncms  25105  cnfldcusp  25107  rrxmvallem  25154  ivthicc  25209  ovolfioo  25218  ovolficc  25219  ovolficcss  25220  ovollb2lem  25239  ovoliunlem2  25254  ovolshftlem1  25260  ovolicc2  25273  ismbl  25277  voliunlem2  25302  volsup  25307  ioorf  25324  ioorinv  25327  ioorcl  25328  uniiccdif  25329  uniioovol  25330  uniiccvol  25331  uniioombllem2  25334  uniioombllem4  25337  dyaddisj  25347  dyadmax  25349  dyadmbllem  25350  dyadmbl  25351  opnmbllem  25352  opnmblALT  25354  volsup2  25356  mbfdm  25377  mbfima  25381  mbfid  25386  ismbfd  25390  mbfres2  25396  mbfposr  25403  mbfimaopnlem  25406  mbflimsup  25417  0plef  25423  i1f1lem  25440  itg11  25442  itg1addlem4  25450  itg1addlem4OLD  25451  i1fpos  25458  itg1le  25465  itg1climres  25466  mbfi1fseqlem5  25471  mbfi1flimlem  25474  xrge0f  25483  itg2ge0  25487  itg2seq  25494  itg2i1fseqle  25506  itg2i1fseq2  25508  itg2addlem  25510  itg2gt0  25512  limciun  25645  dvres  25662  dvres3a  25665  cpnres  25688  dvfre  25702  dvmptres3  25707  dvlip2  25746  dvgt0lem2  25754  deg1fvi  25837  uc1pmon1p  25903  fta1g  25919  ig1peu  25923  ig1pdvds  25928  plyco0  25940  plypf1  25960  dgrlem  25977  dgrub  25982  dgrlb  25984  coemulc  26003  plyreres  26030  plydivlem3  26042  plydivlem4  26043  plydiveu  26045  plyremlem  26051  fta1lem  26054  fta1  26055  vieta1lem2  26058  plyexmo  26060  elaa  26063  elqaalem3  26068  aannenlem1  26075  pserulm  26168  psercnlem2  26170  psercnlem1  26171  psercn  26172  abelth  26187  reeff1o  26193  pilem1  26197  recosf1o  26278  resinf1o  26279  efif1olem3  26287  efif1olem4  26288  efifo  26290  eff1olem  26291  ellogrn  26302  logcn  26389  dvloglem  26390  logf1o2  26392  efopnlem1  26398  efopnlem2  26399  efopn  26400  logtayl  26402  cxpcn3lem  26489  cxpcn3  26490  resqrtcn  26491  asinneg  26625  areambl  26697  emcllem7  26740  lgamgulm2  26774  basellem4  26822  sqff1o  26920  dvdsmulf1o  26932  fsumdvdsmul  26933  ostthlem1  27364  ostth  27376  noetasuplem4  27473  madeval2  27583  elold  27599  old1  27605  madeoldsuc  27614  tglnfn  28063  f1otrg  28387  axlowdimlem6  28470  axlowdimlem8  28472  axlowdimlem9  28473  axlowdimlem11  28475  axlowdimlem12  28476  axlowdimlem17  28481  elntg2  28508  crctcshlem4  29339  clwlkclwwlklem2  29518  eucrct2eupth  29763  ex-fpar  29980  cnnvm  30200  sspmlem  30250  nvo00  30279  nmlno0lem  30311  phoeqi  30375  ubthlem1  30388  hhip  30695  hhssabloilem  30779  hhssnv  30782  hhsssh  30787  occllem  30821  shsel  30832  chscllem2  31156  df0op2  31270  hoeq  31278  hocofni  31285  hoaddfni  31288  hosubfni  31289  hon0  31311  ho01i  31346  hoeq1  31348  elnlfn  31446  nmlnop0iALT  31513  lnopco0i  31522  imaelshi  31576  nlelchi  31579  rnbra  31625  cnvbraval  31628  kbass5  31638  hmopidmchi  31669  hmopidmpji  31670  foresf1o  32007  fimarab  32133  fcomptf  32148  ofpreima  32155  resf1o  32220  maprnin  32221  fpwrelmapffslem  32222  hashgt1  32285  s3clhash  32379  gsumpart  32475  xrge0tsmsd  32477  tocyc01  32545  cyc3evpm  32577  cycpmgcl  32580  cycpmconjslem2  32582  cyc3conja  32584  kerunit  32705  dimval  32971  dimvalfi  32972  ply1degltdimlem  32993  ply1degltdim  32994  elirng  33037  txomap  33110  locfinreflem  33116  hauseqcn  33174  xpinpreima  33182  xpinpreima2  33183  tpr2rico  33188  mndpluscn  33202  rmulccn  33204  raddcn  33205  xrge0pluscn  33216  xrge0tmdALT  33222  rge0scvg  33225  pl1cn  33231  elzrhunit  33255  qqhf  33262  cnrrext  33286  qqhre  33296  indpi1  33314  indpreima  33319  1stmbfm  33555  2ndmbfm  33556  mbfmcnt  33563  omssubadd  33595  carsggect  33613  eulerpartlemsv2  33653  eulerpartlems  33655  eulerpartlemv  33659  eulerpartlemb  33663  eulerpartlemf  33665  eulerpartlemt  33666  eulerpartlemmf  33670  eulerpartlemgvv  33671  eulerpartlemgh  33673  eulerpartlemgs2  33675  sseqmw  33686  sseqf  33687  sseqp1  33690  fiblem  33693  fibp1  33696  plymul02  33853  signsvtn0  33877  signstres  33882  signshlen  33897  reprinrn  33926  circlemethhgt  33951  txsconnlem  34527  iccllysconn  34537  rellysconn  34538  cvmseu  34563  cvmliftmolem2  34569  cvmliftlem6  34577  cvmliftlem7  34578  cvmliftlem8  34579  cvmliftlem9  34580  cvmliftlem11  34582  cvmliftlem15  34585  cvmlift2lem7  34596  cvmlift2lem10  34599  cvmlift3lem8  34613  cvmlift3lem9  34614  mvrsfpw  34793  mrsubff1  34801  msrid  34832  msrfo  34833  elmsta  34835  mtyf  34839  msubff1  34843  vhmcls  34853  mclsax  34856  elmthm  34863  mthmblem  34867  mclsppslem  34870  iprodefisumlem  35012  fullfunfnv  35220  fullfunfv  35221  gg-dfcnfld  35475  tailfb  35567  filnetlem4  35571  taupilem3  36505  icoreresf  36538  icoreelrnab  36540  relowlssretop  36549  relowlpssretop  36550  unccur  36776  matunitlindflem1  36789  matunitlindflem2  36790  ptrecube  36793  poimirlem28  36821  poimirlem32  36825  heicant  36828  opnmbllem0  36829  mblfinlem1  36830  mblfinlem2  36831  volsupnfl  36838  cnambfre  36841  dvtan  36843  itg2addnclem  36844  itg2addnclem2  36845  ftc1anclem3  36868  ftc1anclem5  36870  ftc1anclem7  36872  ftc1anclem8  36873  ftc1anc  36874  areacirc  36886  indexdom  36907  sdclem2  36915  sstotbnd2  36947  sstotbnd  36948  isbndx  36955  isbnd3b  36958  prdsbnd  36966  prdstotbnd  36967  ismtyhmeolem  36977  heibor1lem  36982  heiborlem1  36984  heibor  36994  rrnequiv  37008  keridl  37205  ellkr  38264  lkr0f  38269  cdleme50rnlem  39720  sticksstones11  41280  sticksstones19  41289  sticksstones22  41292  fsuppind  41466  elrfirn  41737  ismrcd2  41741  isnacs2  41748  nacsfix  41754  mapfzcons1  41759  mzpcompact2lem  41793  eq0rabdioph  41818  eldioph4b  41853  diophren  41855  pw2f1ocnv  42080  pw2f1o2val2  42083  lmhmfgsplit  42132  pwssplit4  42135  hbt  42176  mpaaeu  42196  mendring  42238  proot1mul  42245  proot1hash  42246  proot1ex  42247  deg1mhm  42253  fgraphopab  42256  hausgraph  42258  nvocnvb  42477  ofsubid  43387  expgrowthi  43396  expgrowth  43398  binomcxplemdvbinom  43416  binomcxplemcvg  43417  binomcxplemnotnn0  43419  rfcnpre1  44007  rfcnpre2  44019  cncmpmax  44020  rfcnpre3  44021  rfcnpre4  44022  elixpconstg  44081  ffi  44172  islptre  44635  resincncf  44891  dvcosre  44928  dvresntr  44934  volioof  45003  stoweidlem48  45064  fourierdlem12  45135  fourierdlem15  45138  fourierdlem41  45164  fourierdlem42  45165  fourierdlem46  45168  fourierdlem48  45170  fourierdlem49  45171  fourierdlem54  45176  fourierdlem56  45178  fourierdlem62  45184  fourierdlem64  45186  fourierdlem65  45187  fourierdlem73  45195  fourierdlem74  45196  fourierdlem75  45197  fourierdlem102  45224  fourierdlem103  45225  fourierdlem104  45226  fourierdlem114  45236  sge0split  45425  elhoi  45558  mbfresmf  45755  cfsetsnfsetf1  46069  cfsetsnfsetfo  46070  focofob  46088  f1ocof1ob  46089  fafvelcdm  46178  ffnafv  46179  fafv2elcdm  46242  fafv2elrnb  46243  imarnf1pr  46290  2ffzoeq  46336  fundcmpsurbijinjpreimafv  46375  fundcmpsurinjimaid  46379  fargshiftfv  46407  fargshiftf  46408  fargshiftf1  46409  fargshiftfo  46410  zrinitorngc  46988  zrtermorngc  46989  zrtermoringc  47058  fdmdifeqresdif  47107  fdivmpt  47315  fdivmptf  47316  refdivmptf  47317  1arymaptf1  47417  2arymaptf1  47428  ackfnnn0  47460  aacllem  47937