Theorem ffn 6663

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

Syntax hints:   → wi 4   ⊆ wss 3902  ran crn 5626   Fn wfn 6488  ⟶wf 6489

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 6497

This theorem is referenced by:  ffnd  6664  ffun  6666  frel  6668  fdm  6672  ffrn  6676  fresin  6704  fresaun  6706  fresaunres2  6707  fcoi1  6709  feu  6711  f0bi  6718  dffo2  6751  fimadmfo  6756  fdmeu  6891  feqmptdf  6905  fimarab  6909  fvco3  6934  ffvelcdm  7028  dff2  7046  dffo3  7049  dffo4  7050  dffo5  7051  dffo3f  7053  f1ompt  7058  ffnfv  7066  fcdmssb  7069  fcompt  7080  fsn2  7083  fprb  7142  fconst2g  7151  fpr2g  7159  fex  7174  dff13  7202  nvocnv  7229  soisores  7275  fdmexb  7851  resf1extb  7878  fo1stres  7961  fo2ndres  7962  1stcof  7965  2ndcof  7966  curry1f  8050  curry2f  8052  fparlem1  8056  fparlem2  8057  fo2ndf  8065  soseq  8103  tposf2  8194  smo11  8298  fsetexb  8805  mapsnd  8828  pw2f1olem  9013  mapen  9073  mapunen  9078  fissuni  9261  fipreima  9262  indexfi  9264  mapfien  9315  oismo  9449  cantnflt  9585  cantnfp1lem3  9593  cantnflem4  9605  tcrank  9800  updjudhcoinlf  9848  updjudhcoinrg  9849  updjud  9850  infpwfien  9976  cardinfima  10011  dfacacn  10056  cfflb  10173  cofsmo  10183  cfcoflem  10186  coftr  10187  fin23lem40  10265  axdc3lem2  10365  ac6num  10393  ac6c4  10395  ac6s2  10400  ttukeylem6  10428  iunfo  10453  pwcfsdom  10498  fpwwe2lem5  10550  fpwwe2lem7  10552  pwfseqlem3  10575  inar1  10690  tskcard  10696  tskuni  10698  tskurn  10704  gruima  10717  nqerrel  10847  recmulnq  10879  dmrecnq  10883  axpre-sup  11084  ofsubeq0  12146  dfz2  12511  uzn0  12772  rpnnen1lem3  12896  rpnnen1lem5  12898  unirnioo  13369  dfioo2  13370  ioorebas  13371  fseq1p1m1  13518  2ffzeq  13569  fvinim0ffz  13709  injresinjlem  13710  fsequb2  13903  fseqsupcl  13904  fseqsupubi  13905  ser0f  13982  hashgval  14260  hashinf  14262  hashresfn  14267  ffz0hash  14374  fnfzo0hash  14377  wrdred1hash  14488  revlen  14689  revrev  14694  repswlen  14703  repsdf2  14705  cshword  14718  0csh0  14720  lenco  14759  s1co  14760  cshco  14763  swrdco  14764  s7f1o  14893  ofccat  14896  shftf  15006  uzin2  15272  rexanuz  15273  limsuple  15405  limsupval2  15407  rlimres  15485  lo1res  15486  rlimresb  15492  isercolllem2  15593  isercolllem3  15594  isercoll  15595  supcvg  15783  prodf1f  15819  eff2  16028  reeff1  16049  tanval  16057  ruclem4  16163  ruclem12  16170  prmreclem6  16853  1arithlem4  16858  1arith  16859  vdwmc  16910  vdwlem1  16913  vdwlem8  16920  vdwlem13  16925  ramval  16940  0ram  16952  0ram2  16953  0ramcl  16955  ramcl  16961  fsets  17100  firest  17356  0ssc  17765  0subcat  17766  isfull2  17841  arwhoma  17973  gsumval2a  18614  isgrpinv  18927  kerf1ghm  19180  f1omvdconj  19379  pmtrmvd  19389  pmtrfinv  19394  pmtrdifellem4  19412  efgsfo  19672  efgredlem  19680  efgcpbllemb  19688  frgpup3lem  19710  0frgp  19712  gexex  19786  torsubg  19787  gsumval3  19840  gsumzres  19842  gsummptmhm  19873  gsumzoppg  19877  dprdf1o  19967  dprd2db  19978  zrinitorngc  20579  zrtermorngc  20580  zrtermoringc  20612  srngf1o  20785  lmhmima  21003  lmhmpreima  21004  lmhmrnlss  21006  lspextmo  21012  pwssplit1  21015  cnfldadd  21319  cnfldmul  21321  dfcnfldOLD  21329  cnfldplusf  21355  cnfldsub  21356  chrrhm  21490  znunit  21522  psgnevpmb  21546  psgndiflemB  21559  mpofrlmd  21736  frlmipval  21738  frlmphl  21740  frlmlbs  21756  frlmup4  21760  ellspd  21761  lindfmm  21786  lsslindf  21789  psrbaglefi  21886  psrlidm  21921  mplmonmul  21995  evlseu  22042  mpfconst  22068  mpfproj  22069  mpfsubrg  22070  coe1sclmulfv  22229  pf1const  22294  pf1id  22295  pf1subrg  22296  mpfpf1  22299  pf1mpf  22300  mamuass  22350  mamudi  22351  mamudir  22352  mamuvs1  22353  mamuvs2  22354  1mavmul  22496  mavmulass  22497  mdetunilem7  22566  madutpos  22590  lecldbas  23167  lmbr2  23207  cncnpi  23226  cncnp  23228  cnpdis  23241  lmff  23249  pnrmopn  23291  dnsconst  23326  cmpsub  23348  tgcmp  23349  hauscmplem  23354  2ndcctbss  23403  2ndcomap  23406  2ndcsep  23407  1stccnp  23410  kgenidm  23495  iskgen2  23496  1stckgen  23502  kgen2cn  23507  ptpjpre1  23519  pttop  23530  ptuni  23542  ptval2  23549  tx1cn  23557  tx2cn  23558  ptpjcn  23559  ptpjopn  23560  ptclsg  23563  ptcnplem  23569  upxp  23571  txcnmpt  23572  uptx  23573  txcmplem2  23590  txkgen  23600  xkoptsub  23602  xkopt  23603  xkococnlem  23607  xkococn  23608  ptcmpfi  23761  zfbas  23844  uzrest  23845  rnelfmlem  23900  rnelfm  23901  fmfnfmlem2  23903  fmfnfm  23906  lmflf  23953  alexsubALT  23999  clssubg  24057  qustgplem  24069  tsmsres  24092  tsmsxplem1  24101  ucncn  24232  xmettpos  24297  imasdsf1olem  24321  blrnps  24356  blrn  24357  xmeterval  24380  tmslem  24430  tmsxms  24434  imasf1oxms  24437  prdsxms  24478  blval2  24510  metuel2  24513  isngp2  24545  isngp3  24546  tngngp2  24600  isnghm  24671  qtopbaslem  24706  qdensere  24717  cnbl0  24721  cnblcld  24722  cnfldms  24723  blssioo  24743  tgioo  24744  tgqioo  24748  xrtgioo  24755  xrsdsre  24759  xrge0tsms  24783  iimulcnOLD  24895  bndth  24917  lebnumlem3  24922  nmhmcn  25080  cphsqrtcl  25144  lmmbr2  25219  caucfil  25243  causs  25258  lmcau  25273  bcth3  25291  cncms  25315  cnfldcusp  25317  rrxmvallem  25364  ivthicc  25419  ovolfioo  25428  ovolficc  25429  ovolficcss  25430  ovollb2lem  25449  ovoliunlem2  25464  ovolshftlem1  25470  ovolicc2  25483  ismbl  25487  voliunlem2  25512  volsup  25517  ioorf  25534  ioorinv  25537  ioorcl  25538  uniiccdif  25539  uniioovol  25540  uniiccvol  25541  uniioombllem2  25544  uniioombllem4  25547  dyaddisj  25557  dyadmax  25559  dyadmbllem  25560  dyadmbl  25561  opnmbllem  25562  opnmblALT  25564  volsup2  25566  mbfdm  25587  mbfima  25591  mbfid  25596  ismbfd  25600  mbfres2  25606  mbfposr  25613  mbfimaopnlem  25616  mbflimsup  25627  0plef  25633  i1f1lem  25650  itg11  25652  itg1addlem4  25660  i1fpos  25667  itg1le  25674  itg1climres  25675  mbfi1fseqlem5  25680  mbfi1flimlem  25683  xrge0f  25692  itg2ge0  25696  itg2seq  25703  itg2i1fseqle  25715  itg2i1fseq2  25717  itg2addlem  25719  itg2gt0  25721  limciun  25855  dvres  25872  dvres3a  25875  cpnres  25899  dvfre  25915  dvmptres3  25920  dvlip2  25960  dvgt0lem2  25968  deg1fvi  26050  uc1pmon1p  26117  fta1g  26135  ig1peu  26140  ig1pdvds  26145  plyco0  26157  plypf1  26177  dgrlem  26194  dgrub  26199  dgrlb  26201  coemulc  26220  plyreres  26250  plydivlem3  26263  plydivlem4  26264  plydiveu  26266  plyremlem  26272  fta1lem  26275  fta1  26276  vieta1lem2  26279  plyexmo  26281  elaa  26284  elqaalem3  26289  aannenlem1  26296  pserulm  26391  psercnlem2  26394  psercnlem1  26395  psercn  26396  abelth  26411  reeff1o  26417  pilem1  26421  recosf1o  26504  resinf1o  26505  efif1olem3  26513  efif1olem4  26514  efifo  26516  eff1olem  26517  ellogrn  26528  logcn  26616  dvloglem  26617  logf1o2  26619  efopnlem1  26625  efopnlem2  26626  efopn  26627  logtayl  26629  cxpcn3lem  26717  cxpcn3  26718  resqrtcn  26719  asinneg  26856  areambl  26928  emcllem7  26972  lgamgulm2  27006  basellem4  27054  sqff1o  27152  mpodvdsmulf1o  27164  fsumdvdsmul  27165  dvdsmulf1o  27166  fsumdvdsmulOLD  27167  ostthlem1  27598  ostth  27610  noetasuplem4  27708  madeval2  27831  elold  27851  old1  27857  madeoldsuc  27867  tglnfn  28602  f1otrg  28926  axlowdimlem6  29003  axlowdimlem8  29005  axlowdimlem9  29006  axlowdimlem11  29008  axlowdimlem12  29009  axlowdimlem17  29014  elntg2  29041  dfpth2  29785  cyclnumvtx  29856  crctcshlem4  29876  clwlkclwwlklem2  30058  eucrct2eupth  30303  ex-fpar  30520  cnnvm  30740  sspmlem  30790  nvo00  30819  nmlno0lem  30851  phoeqi  30915  ubthlem1  30928  hhip  31235  hhssabloilem  31319  hhssnv  31322  hhsssh  31327  occllem  31361  shsel  31372  chscllem2  31696  df0op2  31810  hoeq  31818  hocofni  31825  hoaddfni  31828  hosubfni  31829  hon0  31851  ho01i  31886  hoeq1  31888  elnlfn  31986  nmlnop0iALT  32053  lnopco0i  32062  imaelshi  32116  nlelchi  32119  rnbra  32165  cnvbraval  32168  kbass5  32178  hmopidmchi  32209  hmopidmpji  32210  foresf1o  32561  fcomptf  32718  ofpreima  32725  resf1o  32790  maprnin  32791  fpwrelmapffslem  32792  hashgt1  32869  indpi1  32922  indpreima  32928  s3clhash  33011  gsumpart  33127  xrge0tsmsd  33136  tocyc01  33181  cyc3evpm  33213  cycpmgcl  33216  cycpmconjslem2  33218  cyc3conja  33220  kerunit  33387  1arithidomlem1  33597  1arithidomlem2  33598  1arithidom  33599  dimval  33738  dimvalfi  33739  ply1degltdimlem  33760  ply1degltdim  33761  elirng  33824  txomap  33972  locfinreflem  33978  hauseqcn  34036  xpinpreima  34044  xpinpreima2  34045  tpr2rico  34050  mndpluscn  34064  raddcn  34067  xrge0pluscn  34078  xrge0tmdALT  34084  rge0scvg  34087  pl1cn  34093  elzrhunit  34115  qqhf  34124  cnrrext  34148  qqhre  34158  1stmbfm  34398  2ndmbfm  34399  mbfmcnt  34406  omssubadd  34438  carsggect  34456  eulerpartlemsv2  34496  eulerpartlems  34498  eulerpartlemv  34502  eulerpartlemb  34506  eulerpartlemf  34508  eulerpartlemt  34509  eulerpartlemmf  34513  eulerpartlemgvv  34514  eulerpartlemgh  34516  eulerpartlemgs2  34518  sseqmw  34529  sseqf  34530  sseqp1  34533  fiblem  34536  fibp1  34539  plymul02  34684  signsvtn0  34708  signstres  34713  signshlen  34728  reprinrn  34756  circlemethhgt  34781  txsconnlem  35415  iccllysconn  35425  rellysconn  35426  cvmseu  35451  cvmliftmolem2  35457  cvmliftlem6  35465  cvmliftlem7  35466  cvmliftlem8  35467  cvmliftlem9  35468  cvmliftlem11  35470  cvmliftlem15  35473  cvmlift2lem7  35484  cvmlift2lem10  35487  cvmlift3lem8  35501  cvmlift3lem9  35502  mvrsfpw  35681  mrsubff1  35689  msrid  35720  msrfo  35721  elmsta  35723  mtyf  35727  msubff1  35731  vhmcls  35741  mclsax  35744  elmthm  35751  mthmblem  35755  mclsppslem  35758  iprodefisumlem  35915  fullfunfnv  36121  fullfunfv  36122  tailfb  36552  filnetlem4  36556  taupilem3  37495  icoreresf  37528  icoreelrnab  37530  relowlssretop  37539  relowlpssretop  37540  unccur  37775  matunitlindflem1  37788  matunitlindflem2  37789  ptrecube  37792  poimirlem28  37820  poimirlem32  37824  heicant  37827  opnmbllem0  37828  mblfinlem1  37829  mblfinlem2  37830  volsupnfl  37837  cnambfre  37840  dvtan  37842  itg2addnclem  37843  itg2addnclem2  37844  ftc1anclem3  37867  ftc1anclem5  37869  ftc1anclem7  37871  ftc1anclem8  37872  ftc1anc  37873  areacirc  37885  indexdom  37906  sdclem2  37914  sstotbnd2  37946  sstotbnd  37947  isbndx  37954  isbnd3b  37957  prdsbnd  37965  prdstotbnd  37966  ismtyhmeolem  37976  heibor1lem  37981  heiborlem1  37983  heibor  37993  rrnequiv  38007  keridl  38204  ellkr  39386  lkr0f  39391  cdleme50rnlem  40841  aks6d1c2lem4  42418  aks6d1c5  42430  sticksstones11  42447  sticksstones19  42456  sticksstones22  42459  aks6d1c6lem4  42464  aks6d1c6isolem2  42466  fsuppind  42869  elrfirn  42973  ismrcd2  42977  isnacs2  42984  nacsfix  42990  mapfzcons1  42995  mzpcompact2lem  43029  eq0rabdioph  43054  eldioph4b  43089  diophren  43091  pw2f1ocnv  43315  pw2f1o2val2  43318  lmhmfgsplit  43364  pwssplit4  43367  hbt  43408  mpaaeu  43428  mendring  43466  proot1mul  43472  proot1hash  43473  proot1ex  43474  deg1mhm  43478  fgraphopab  43481  hausgraph  43483  nvocnvb  43699  ofsubid  44601  expgrowthi  44610  expgrowth  44612  binomcxplemdvbinom  44630  binomcxplemcvg  44631  binomcxplemnotnn0  44633  relpfrlem  45230  rfcnpre1  45300  rfcnpre2  45312  cncmpmax  45313  rfcnpre3  45314  rfcnpre4  45315  elixpconstg  45369  ffi  45453  islptre  45901  resincncf  46155  dvcosre  46192  dvresntr  46198  volioof  46267  stoweidlem48  46328  fourierdlem12  46399  fourierdlem15  46402  fourierdlem41  46428  fourierdlem42  46429  fourierdlem46  46432  fourierdlem48  46434  fourierdlem49  46435  fourierdlem54  46440  fourierdlem56  46442  fourierdlem62  46448  fourierdlem64  46450  fourierdlem65  46451  fourierdlem73  46459  fourierdlem74  46460  fourierdlem75  46461  fourierdlem102  46488  fourierdlem103  46489  fourierdlem104  46490  fourierdlem114  46500  sge0split  46689  elhoi  46822  mbfresmf  47019  cjnpoly  47171  cfsetsnfsetf1  47341  cfsetsnfsetfo  47342  focofob  47362  f1ocof1ob  47363  fafvelcdm  47452  ffnafv  47453  fafv2elcdm  47516  fafv2elrnb  47517  imarnf1pr  47564  2ffzoeq  47609  fundcmpsurbijinjpreimafv  47689  fundcmpsurinjimaid  47693  fargshiftfv  47721  fargshiftf  47722  fargshiftf1  47723  fargshiftfo  47724  cycl3grtri  48229  fdmdifeqresdif  48624  fdivmpt  48822  fdivmptf  48823  refdivmptf  48824  1arymaptf1  48924  2arymaptf1  48935  ackfnnn0  48967  homf0  49290  aacllem  50082