Theorem ffn 6715

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

Syntax hints:   → wi 4   ⊆ wss 3948  ran crn 5677   Fn wfn 6536  ⟶wf 6537

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 398  df-f 6545

This theorem is referenced by:  ffnd  6716  ffun  6718  frel  6720  fdm  6724  fdmOLD  6725  ffrn  6729  fresin  6758  fresaun  6760  fresaunres2  6761  fcoi1  6763  feu  6765  f0bi  6772  dffo2  6807  fimadmfo  6812  feqmptdf  6960  fvco3  6988  ffvelcdm  7081  dff2  7098  dffo3  7101  dffo4  7102  dffo5  7103  f1ompt  7108  ffnfv  7115  fcdmssb  7118  fcompt  7128  fsn2  7131  fprb  7192  fconst2g  7201  fpr2g  7210  fex  7225  dff13  7251  nvocnv  7276  soisores  7321  fdmexb  7897  fo1stres  7998  fo2ndres  7999  1stcof  8002  2ndcof  8003  curry1f  8089  curry2f  8091  fparlem1  8095  fparlem2  8096  fo2ndf  8104  soseq  8142  tposf2  8232  smo11  8361  fsetexb  8855  mapsnd  8877  pw2f1olem  9073  mapen  9138  mapunen  9143  fissuni  9354  fipreima  9355  indexfi  9357  mapfien  9400  oismo  9532  cantnflt  9664  cantnfp1lem3  9672  cantnflem4  9684  tcrank  9876  updjudhcoinlf  9924  updjudhcoinrg  9925  updjud  9926  infpwfien  10054  cardinfima  10089  dfacacn  10133  cfflb  10251  cofsmo  10261  cfcoflem  10264  coftr  10265  fin23lem40  10343  axdc3lem2  10443  ac6num  10471  ac6c4  10473  ac6s2  10478  ttukeylem6  10506  iunfo  10531  pwcfsdom  10575  fpwwe2lem5  10627  fpwwe2lem7  10629  pwfseqlem3  10652  inar1  10767  tskcard  10773  tskuni  10775  tskurn  10781  gruima  10794  nqerrel  10924  recmulnq  10956  dmrecnq  10960  axpre-sup  11161  ofsubeq0  12206  dfz2  12574  uzn0  12836  rpnnen1lem3  12960  rpnnen1lem5  12962  unirnioo  13423  dfioo2  13424  ioorebas  13425  fseq1p1m1  13572  2ffzeq  13619  fvinim0ffz  13748  injresinjlem  13749  fsequb2  13938  fseqsupcl  13939  fseqsupubi  13940  ser0f  14018  hashgval  14290  hashinf  14292  hashresfn  14297  ffz0hash  14403  fnfzo0hash  14406  wrdred1hash  14508  revlen  14709  revrev  14714  repswlen  14723  repsdf2  14725  cshword  14738  0csh0  14740  lenco  14780  s1co  14781  cshco  14784  swrdco  14785  ofccat  14913  shftf  15023  uzin2  15288  rexanuz  15289  limsuple  15419  limsupval2  15421  rlimres  15499  lo1res  15500  rlimresb  15506  isercolllem2  15609  isercolllem3  15610  isercoll  15611  supcvg  15799  prodf1f  15835  eff2  16039  reeff1  16060  tanval  16068  ruclem4  16174  ruclem12  16181  prmreclem6  16851  1arithlem4  16856  1arith  16857  vdwmc  16908  vdwlem1  16911  vdwlem8  16918  vdwlem13  16923  ramval  16938  0ram  16950  0ram2  16951  0ramcl  16953  ramcl  16959  fsets  17099  firest  17375  0ssc  17784  0subcat  17785  isfull2  17859  arwhoma  17992  gsumval2a  18601  isgrpinv  18875  f1omvdconj  19309  pmtrmvd  19319  pmtrfinv  19324  pmtrdifellem4  19342  efgsfo  19602  efgredlem  19610  efgcpbllemb  19618  frgpup3lem  19640  0frgp  19642  gexex  19716  torsubg  19717  gsumval3  19770  gsumzres  19772  gsummptmhm  19803  gsumzoppg  19807  dprdf1o  19897  dprd2db  19908  kerf1ghm  20275  srngf1o  20455  lmhmima  20651  lmhmpreima  20652  lmhmrnlss  20654  lspextmo  20660  pwssplit1  20663  cnfldplusf  20965  cnfldsub  20966  chrrhm  21075  znunit  21111  psgnevpmb  21132  psgndiflemB  21145  mpofrlmd  21324  frlmipval  21326  frlmphl  21328  frlmlbs  21344  frlmup4  21348  ellspd  21349  lindfmm  21374  lsslindf  21377  psrbaglefi  21477  psrbaglefiOLD  21478  psrlidm  21515  mplmonmul  21583  evlseu  21638  mpfconst  21656  mpfproj  21657  mpfsubrg  21658  coe1sclmulfv  21797  pf1const  21857  pf1id  21858  pf1subrg  21859  mpfpf1  21862  pf1mpf  21863  mamuass  21894  mamudi  21895  mamudir  21896  mamuvs1  21897  mamuvs2  21898  1mavmul  22042  mavmulass  22043  mdetunilem7  22112  madutpos  22136  lecldbas  22715  lmbr2  22755  cncnpi  22774  cncnp  22776  cnpdis  22789  lmff  22797  pnrmopn  22839  dnsconst  22874  cmpsub  22896  tgcmp  22897  hauscmplem  22902  2ndcctbss  22951  2ndcomap  22954  2ndcsep  22955  1stccnp  22958  kgenidm  23043  iskgen2  23044  1stckgen  23050  kgen2cn  23055  ptpjpre1  23067  pttop  23078  ptuni  23090  ptval2  23097  tx1cn  23105  tx2cn  23106  ptpjcn  23107  ptpjopn  23108  ptclsg  23111  ptcnplem  23117  upxp  23119  txcnmpt  23120  uptx  23121  txcmplem2  23138  txkgen  23148  xkoptsub  23150  xkopt  23151  xkococnlem  23155  xkococn  23156  ptcmpfi  23309  zfbas  23392  uzrest  23393  rnelfmlem  23448  rnelfm  23449  fmfnfmlem2  23451  fmfnfm  23454  lmflf  23501  alexsubALT  23547  clssubg  23605  qustgplem  23617  tsmsres  23640  tsmsxplem1  23649  ucncn  23782  xmettpos  23847  imasdsf1olem  23871  blrnps  23906  blrn  23907  xmeterval  23930  tmslem  23982  tmslemOLD  23983  tmsxms  23987  imasf1oxms  23990  prdsxms  24031  blval2  24063  metuel2  24066  isngp2  24098  isngp3  24099  tngngp2  24161  isnghm  24232  qtopbaslem  24267  qdensere  24278  cnbl0  24282  cnblcld  24283  cnfldms  24284  blssioo  24303  tgioo  24304  tgqioo  24308  xrtgioo  24314  xrsdsre  24318  xrge0tsms  24342  iimulcn  24446  bndth  24466  lebnumlem3  24471  nmhmcn  24628  cphsqrtcl  24693  lmmbr2  24768  caucfil  24792  causs  24807  lmcau  24822  bcth3  24840  cncms  24864  cnfldcusp  24866  rrxmvallem  24913  ivthicc  24967  ovolfioo  24976  ovolficc  24977  ovolficcss  24978  ovollb2lem  24997  ovoliunlem2  25012  ovolshftlem1  25018  ovolicc2  25031  ismbl  25035  voliunlem2  25060  volsup  25065  ioorf  25082  ioorinv  25085  ioorcl  25086  uniiccdif  25087  uniioovol  25088  uniiccvol  25089  uniioombllem2  25092  uniioombllem4  25095  dyaddisj  25105  dyadmax  25107  dyadmbllem  25108  dyadmbl  25109  opnmbllem  25110  opnmblALT  25112  volsup2  25114  mbfdm  25135  mbfima  25139  mbfid  25144  ismbfd  25148  mbfres2  25154  mbfposr  25161  mbfimaopnlem  25164  mbflimsup  25175  0plef  25181  i1f1lem  25198  itg11  25200  itg1addlem4  25208  itg1addlem4OLD  25209  i1fpos  25216  itg1le  25223  itg1climres  25224  mbfi1fseqlem5  25229  mbfi1flimlem  25232  xrge0f  25241  itg2ge0  25245  itg2seq  25252  itg2i1fseqle  25264  itg2i1fseq2  25266  itg2addlem  25268  itg2gt0  25270  limciun  25403  dvres  25420  dvres3a  25423  cpnres  25446  dvfre  25460  dvmptres3  25465  dvlip2  25504  dvgt0lem2  25512  deg1fvi  25595  uc1pmon1p  25661  fta1g  25677  ig1peu  25681  ig1pdvds  25686  plyco0  25698  plypf1  25718  dgrlem  25735  dgrub  25740  dgrlb  25742  coemulc  25761  plyreres  25788  plydivlem3  25800  plydivlem4  25801  plydiveu  25803  plyremlem  25809  fta1lem  25812  fta1  25813  vieta1lem2  25816  plyexmo  25818  elaa  25821  elqaalem3  25826  aannenlem1  25833  pserulm  25926  psercnlem2  25928  psercnlem1  25929  psercn  25930  abelth  25945  reeff1o  25951  pilem1  25955  recosf1o  26036  resinf1o  26037  efif1olem3  26045  efif1olem4  26046  efifo  26048  eff1olem  26049  ellogrn  26060  logcn  26147  dvloglem  26148  logf1o2  26150  efopnlem1  26156  efopnlem2  26157  efopn  26158  logtayl  26160  cxpcn3lem  26245  cxpcn3  26246  resqrtcn  26247  asinneg  26381  areambl  26453  emcllem7  26496  lgamgulm2  26530  basellem4  26578  sqff1o  26676  dvdsmulf1o  26688  fsumdvdsmul  26689  ostthlem1  27120  ostth  27132  noetasuplem4  27229  madeval2  27338  elold  27354  old1  27360  madeoldsuc  27369  tglnfn  27788  f1otrg  28112  axlowdimlem6  28195  axlowdimlem8  28197  axlowdimlem9  28198  axlowdimlem11  28200  axlowdimlem12  28201  axlowdimlem17  28206  elntg2  28233  crctcshlem4  29064  clwlkclwwlklem2  29243  eucrct2eupth  29488  ex-fpar  29705  cnnvm  29923  sspmlem  29973  nvo00  30002  nmlno0lem  30034  phoeqi  30098  ubthlem1  30111  hhip  30418  hhssabloilem  30502  hhssnv  30505  hhsssh  30510  occllem  30544  shsel  30555  chscllem2  30879  df0op2  30993  hoeq  31001  hocofni  31008  hoaddfni  31011  hosubfni  31012  hon0  31034  ho01i  31069  hoeq1  31071  elnlfn  31169  nmlnop0iALT  31236  lnopco0i  31245  imaelshi  31299  nlelchi  31302  rnbra  31348  cnvbraval  31351  kbass5  31361  hmopidmchi  31392  hmopidmpji  31393  foresf1o  31730  fimarab  31856  fcomptf  31871  ofpreima  31878  resf1o  31943  maprnin  31944  fpwrelmapffslem  31945  hashgt1  32008  s3clhash  32102  gsumpart  32195  xrge0tsmsd  32197  tocyc01  32265  cyc3evpm  32297  cycpmgcl  32300  cycpmconjslem2  32302  cyc3conja  32304  kerunit  32426  dimval  32675  dimvalfi  32676  ply1degltdimlem  32696  ply1degltdim  32697  elirng  32739  txomap  32803  locfinreflem  32809  hauseqcn  32867  xpinpreima  32875  xpinpreima2  32876  tpr2rico  32881  mndpluscn  32895  rmulccn  32897  raddcn  32898  xrge0pluscn  32909  xrge0tmdALT  32915  rge0scvg  32918  pl1cn  32924  elzrhunit  32948  qqhf  32955  cnrrext  32979  qqhre  32989  indpi1  33007  indpreima  33012  1stmbfm  33248  2ndmbfm  33249  mbfmcnt  33256  omssubadd  33288  carsggect  33306  eulerpartlemsv2  33346  eulerpartlems  33348  eulerpartlemv  33352  eulerpartlemb  33356  eulerpartlemf  33358  eulerpartlemt  33359  eulerpartlemmf  33363  eulerpartlemgvv  33364  eulerpartlemgh  33366  eulerpartlemgs2  33368  sseqmw  33379  sseqf  33380  sseqp1  33383  fiblem  33386  fibp1  33389  plymul02  33546  signsvtn0  33570  signstres  33575  signshlen  33590  reprinrn  33619  circlemethhgt  33644  txsconnlem  34220  iccllysconn  34230  rellysconn  34231  cvmseu  34256  cvmliftmolem2  34262  cvmliftlem6  34270  cvmliftlem7  34271  cvmliftlem8  34272  cvmliftlem9  34273  cvmliftlem11  34275  cvmliftlem15  34278  cvmlift2lem7  34289  cvmlift2lem10  34292  cvmlift3lem8  34306  cvmlift3lem9  34307  mvrsfpw  34486  mrsubff1  34494  msrid  34525  msrfo  34526  elmsta  34528  mtyf  34532  msubff1  34536  vhmcls  34546  mclsax  34549  elmthm  34556  mthmblem  34560  mclsppslem  34563  iprodefisumlem  34699  fullfunfnv  34907  fullfunfv  34908  tailfb  35251  filnetlem4  35255  taupilem3  36189  icoreresf  36222  icoreelrnab  36224  relowlssretop  36233  relowlpssretop  36234  unccur  36460  matunitlindflem1  36473  matunitlindflem2  36474  ptrecube  36477  poimirlem28  36505  poimirlem32  36509  heicant  36512  opnmbllem0  36513  mblfinlem1  36514  mblfinlem2  36515  volsupnfl  36522  cnambfre  36525  dvtan  36527  itg2addnclem  36528  itg2addnclem2  36529  ftc1anclem3  36552  ftc1anclem5  36554  ftc1anclem7  36556  ftc1anclem8  36557  ftc1anc  36558  areacirc  36570  indexdom  36591  sdclem2  36599  sstotbnd2  36631  sstotbnd  36632  isbndx  36639  isbnd3b  36642  prdsbnd  36650  prdstotbnd  36651  ismtyhmeolem  36661  heibor1lem  36666  heiborlem1  36668  heibor  36678  rrnequiv  36692  keridl  36889  ellkr  37948  lkr0f  37953  cdleme50rnlem  39404  sticksstones11  40961  sticksstones19  40970  sticksstones22  40973  fsuppind  41160  elrfirn  41419  ismrcd2  41423  isnacs2  41430  nacsfix  41436  mapfzcons1  41441  mzpcompact2lem  41475  eq0rabdioph  41500  eldioph4b  41535  diophren  41537  pw2f1ocnv  41762  pw2f1o2val2  41765  lmhmfgsplit  41814  pwssplit4  41817  hbt  41858  mpaaeu  41878  mendring  41920  proot1mul  41927  proot1hash  41928  proot1ex  41929  deg1mhm  41935  fgraphopab  41938  hausgraph  41940  nvocnvb  42159  ofsubid  43069  expgrowthi  43078  expgrowth  43080  binomcxplemdvbinom  43098  binomcxplemcvg  43099  binomcxplemnotnn0  43101  rfcnpre1  43689  rfcnpre2  43701  cncmpmax  43702  rfcnpre3  43703  rfcnpre4  43704  elixpconstg  43764  ffi  43855  dffo3f  43863  islptre  44322  resincncf  44578  dvcosre  44615  dvresntr  44621  volioof  44690  stoweidlem48  44751  fourierdlem12  44822  fourierdlem15  44825  fourierdlem41  44851  fourierdlem42  44852  fourierdlem46  44855  fourierdlem48  44857  fourierdlem49  44858  fourierdlem54  44863  fourierdlem56  44865  fourierdlem62  44871  fourierdlem64  44873  fourierdlem65  44874  fourierdlem73  44882  fourierdlem74  44883  fourierdlem75  44884  fourierdlem102  44911  fourierdlem103  44912  fourierdlem104  44913  fourierdlem114  44923  sge0split  45112  elhoi  45245  mbfresmf  45442  cfsetsnfsetf1  45756  cfsetsnfsetfo  45757  focofob  45775  f1ocof1ob  45776  fafvelcdm  45865  ffnafv  45866  fafv2elcdm  45929  fafv2elrnb  45930  imarnf1pr  45977  2ffzoeq  46023  fundcmpsurbijinjpreimafv  46062  fundcmpsurinjimaid  46066  fargshiftfv  46094  fargshiftf  46095  fargshiftf1  46096  fargshiftfo  46097  zrinitorngc  46852  zrtermorngc  46853  zrtermoringc  46922  fdmdifeqresdif  46971  fdivmpt  47180  fdivmptf  47181  refdivmptf  47182  1arymaptf1  47282  2arymaptf1  47293  ackfnnn0  47325  aacllem  47802