Theorem ffn 6709

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

This proof depends on syntax axioms:   → wi 4   ⊆ wss 3906  ran crn 5664   Fn wfn 6535  ⟶wf 6536

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-f 6544

This theorem is used by:  ffnd  6710  ffun  6712  ffunOLD  6713  frel  6715  fdm  6719  ffrn  6723  fresin  6751  fresaun  6753  fresaunres2  6754  fcoi1  6756  feu  6758  f0bi  6765  dffo2  6800  fimadmfo  6805  fdmeu  6941  feqmptdf  6955  fimarab  6959  fvco3  6985  ffvelcdm  7080  dff2  7098  dffo3  7101  dffo4  7102  dffo5  7103  dffo3f  7105  f1ompt  7110  ffnfv  7118  fcdmssb  7121  fcompt  7133  fsn2  7136  fprb  7196  fconst2g  7205  fpr2g  7213  fex  7228  dff13  7254  nvocnv  7285  soisores  7331  fdmexb  7906  resf1extb  7933  fo1stres  8014  fo2ndres  8015  1stcof  8018  2ndcof  8019  curry1f  8103  curry2f  8105  fparlem1  8109  fparlem2  8110  fo2ndf  8118  soseq  8157  tposf2  8248  smo11  8353  fsetexb  8863  mapsnd  8886  pw2f1olem  9072  mapen  9132  mapunen  9137  fissuni  9317  fipreima  9318  indexfi  9320  mapfien  9371  oismo  9505  cantnflt  9644  cantnfp1lem3  9652  cantnflem4  9664  tcrank  9859  updjudhcoinlf  9930  updjudhcoinrg  9931  updjud  9932  infpwfien  10058  cardinfima  10093  dfacacn  10137  cfflb  10254  cofsmo  10264  cfcoflem  10267  coftr  10268  fin23lem40  10346  axdc3lem2  10446  ac6num  10474  ac6c4  10476  ac6s2  10481  ttukeylem6  10509  iunfo  10534  pwcfsdom  10579  fpwwe2lem5  10631  fpwwe2lem7  10633  pwfseqlem3  10656  inar1  10771  tskcard  10777  tskuni  10779  tskurn  10785  gruima  10798  nqerrel  10928  recmulnq  10960  dmrecnq  10964  axpre-sup  11165  ofsubeq0  12226  indpi1  12243  dfz2  12621  uzn0  12891  rpnnen1lem3  13015  rpnnen1lem5  13017  unirnioo  13488  dfioo2  13489  ioorebas  13490  fseq1p1m1  13639  2ffzeq  13690  fvinim0ffz  13831  injresinjlem  13832  fsequb2  14026  fseqsupcl  14027  fseqsupubi  14028  ser0f  14105  hashgval  14383  hashinf  14385  hashresfn  14390  ffz0hash  14498  fnfzo0hash  14501  wrdred1hash  14612  revlen  14817  revrev  14822  repswlen  14833  repsdf2  14835  cshword  14848  0csh0  14850  lenco  14889  s1co  14890  cshco  14893  swrdco  14894  s7f1o  15023  ofccat  15026  shftf  15136  uzin2  15416  rexanuz  15417  limsuple  15549  limsupval2  15551  rlimres  15629  lo1res  15630  rlimresb  15636  isercolllem2  15737  isercolllem3  15738  isercoll  15739  supcvg  15929  prodf1f  15965  eff2  16173  reeff1  16194  tanval  16202  ruclem4  16308  ruclem12  16315  prmreclem6  16999  1arithlem4  17004  1arith  17005  vdwmc  17056  vdwlem1  17059  vdwlem8  17066  vdwlem13  17071  ramval  17086  0ram  17098  0ram2  17099  0ramcl  17101  ramcl  17107  fsets  17247  firest  17503  0ssc  17912  0subcat  17913  isfull2  17988  arwhoma  18120  gsumval2a  18765  isgrpinv  19084  kerf1ghm  19341  f1omvdconj  19540  pmtrmvd  19550  pmtrfinv  19555  pmtrdifellem4  19573  efgsfo  19833  efgredlem  19841  efgcpbllemb  19849  frgpup3lem  19871  0frgp  19873  gexex  19947  torsubg  19948  gsumval3  20001  gsumzres  20003  gsummptmhm  20034  gsumzoppg  20038  dprdf1o  20128  dprd2db  20139  zrinitorngc  20771  zrtermorngc  20772  zrtermoringc  20804  srngf1o  20981  lmhmima  21198  lmhmpreima  21199  lmhmrnlss  21201  lspextmo  21207  pwssplit1  21210  cnfldadd  21558  cnfldmul  21560  cnfldplusf  21579  cnfldsub  21580  chrrhm  21711  znunit  21743  psgnevpmb  21767  psgndiflemB  21780  mpofrlmd  21957  frlmipval  21959  frlmphl  21961  frlmlbs  21977  frlmup4  21981  ellspd  21982  lindfmm  22007  lsslindf  22010  psrbaglefi  22106  psrlidm  22141  mplmonmul  22217  evlseu  22264  mpfconst  22290  mpfproj  22291  mpfsubrg  22292  coe1sclmulfv  22474  pf1const  22536  pf1id  22537  pf1subrg  22538  mpfpf1  22541  pf1mpf  22542  mamuass  22589  mamudi  22590  mamudir  22591  mamuvs1  22592  mamuvs2  22593  1mavmul  22735  mavmulass  22736  mdetunilem7  22805  madutpos  22829  lecldbas  23406  lmbr2  23446  cncnpi  23465  cncnp  23467  cnpdis  23480  lmff  23488  pnrmopn  23530  dnsconst  23565  cmpsub  23587  tgcmp  23588  hauscmplem  23593  2ndcctbss  23643  2ndcomap  23646  2ndcsep  23647  1stccnp  23650  kgenidm  23735  iskgen2  23736  1stckgen  23742  kgen2cn  23747  ptpjpre1  23759  pttop  23770  ptuni  23782  ptval2  23789  tx1cn  23797  tx2cn  23798  ptpjcn  23799  ptpjopn  23800  ptclsg  23803  ptcnplem  23809  upxp  23811  txcnmpt  23812  uptx  23813  txcmplem2  23830  txkgen  23840  xkoptsub  23842  xkopt  23843  xkococnlem  23847  xkococn  23848  ptcmpfi  24001  zfbas  24084  uzrest  24085  rnelfmlem  24140  rnelfm  24141  fmfnfmlem2  24143  fmfnfm  24146  lmflf  24193  alexsubALT  24239  clssubg  24297  qustgplem  24309  tsmsres  24332  tsmsxplem1  24341  ucncn  24472  xmettpos  24537  imasdsf1olem  24561  blrnps  24596  blrn  24597  xmeterval  24620  tmslem  24670  tmsxms  24674  imasf1oxms  24677  prdsxms  24718  blval2  24750  metuel2  24753  isngp2  24785  isngp3  24786  tngngp2  24840  isnghm  24911  qtopbaslem  24946  qdensere  24957  cnbl0  24961  cnblcld  24962  cnfldms  24963  blssioo  24983  tgioo  24984  tgqioo  24988  xrtgioo  24995  xrsdsre  24999  xrge0tsms  25023  bndth  25148  lebnumlem3  25153  nmhmcn  25310  cphsqrtcl  25374  lmmbr2  25449  caucfil  25473  causs  25488  lmcau  25503  bcth3  25521  cncms  25545  cnfldcusp  25547  rrxmvallem  25594  ivthicc  25648  ovolfioo  25657  ovolficc  25658  ovolficcss  25659  ovollb2lem  25678  ovoliunlem2  25693  ovolshftlem1  25699  ovolicc2  25712  ismbl  25716  voliunlem2  25741  volsup  25746  ioorf  25763  ioorinv  25766  ioorcl  25767  uniiccdif  25768  uniioovol  25769  uniiccvol  25770  uniioombllem2  25773  uniioombllem4  25776  dyaddisj  25786  dyadmax  25788  dyadmbllem  25789  dyadmbl  25790  opnmbllem  25791  opnmblALT  25793  volsup2  25795  mbfdm  25816  mbfima  25820  mbfid  25825  ismbfd  25829  mbfres2  25835  mbfposr  25842  mbfimaopnlem  25845  mbflimsup  25856  0plef  25862  i1f1lem  25879  itg11  25881  itg1addlem4  25889  i1fpos  25896  itg1le  25903  itg1climres  25904  mbfi1fseqlem5  25909  mbfi1flimlem  25912  xrge0f  25921  itg2ge0  25925  itg2seq  25932  itg2i1fseqle  25944  itg2i1fseq2  25946  itg2addlem  25948  itg2gt0  25950  limciun  26084  dvres  26101  dvres3a  26104  cpnres  26127  dvfre  26141  dvmptres3  26146  dvlip2  26185  dvgt0lem2  26193  deg1fvi  26273  uc1pmon1p  26340  fta1g  26358  ig1peu  26363  ig1pdvds  26368  plyco0  26380  plypf1  26400  dgrlem  26417  dgrub  26422  dgrlb  26424  coemulc  26443  plymul02  26472  plyreres  26475  plydivlem3  26487  plydivlem4  26488  plydiveu  26490  plyremlem  26496  fta1lem  26499  fta1  26500  vieta1lem2  26503  plyexmo  26505  elaa  26508  elqaalem3  26513  aannenlem1  26522  pserulm  26616  psercnlem2  26618  psercnlem1  26619  psercn  26620  abelth  26635  reeff1o  26641  pilem1  26645  recosf1o  26731  resinf1o  26732  efif1olem3  26740  efif1olem4  26741  efifo  26743  eff1olem  26744  ellogrn  26755  logcn  26843  dvloglem  26844  logf1o2  26846  efopnlem1  26852  efopnlem2  26853  efopn  26854  logtayl  26856  cxpcn3lem  26943  cxpcn3  26944  resqrtcn  26945  asinneg  27082  areambl  27154  emcllem7  27197  lgamgulm2  27231  basellem4  27279  sqff1o  27377  mpodvdsmulf1o  27389  fsumdvdsmul  27390  dvdsmulf1o  27391  ostthlem1  27822  ostth  27834  noetasuplem4  27931  madeval2  28057  elold  28083  old1  28089  madeoldsuc  28109  tglnfn  28847  tgplnfn  29088  f1otrg  29251  axlowdimlem6  29328  axlowdimlem8  29330  axlowdimlem9  29331  axlowdimlem11  29333  axlowdimlem12  29334  axlowdimlem17  29339  elntg2  29366  dfpth2  30117  cyclnumvtx  30191  crctcshlem4  30212  clwlkclwwlklem2  30394  eucrct2eupth  30643  ex-fpar  30860  cnnvm  31081  sspmlem  31131  nvo00  31160  nmlno0lem  31192  phoeqi  31256  ubthlem1  31269  hhip  31576  hhssabloilem  31660  hhssnv  31663  hhsssh  31668  occllem  31702  shsel  31713  chscllem2  32037  df0op2  32151  hoeq  32159  hocofni  32166  hoaddfni  32169  hosubfni  32170  hon0  32192  ho01i  32227  hoeq1  32229  elnlfn  32327  nmlnop0iALT  32394  lnopco0i  32403  imaelshi  32457  nlelchi  32460  rnbra  32506  cnvbraval  32509  kbass5  32519  hmopidmchi  32550  hmopidmpji  32551  foresf1o  32897  fcomptf  33050  ofpreima  33057  resf1o  33121  maprnin  33122  fpwrelmapffslem  33123  hashgt1  33199  indpreima  33231  s3clhash  33311  gsumpart  33423  xrge0tsmsd  33433  tocyc01  33478  cyc3evpm  33510  cycpmgcl  33513  cycpmconjslem2  33515  cyc3conja  33517  kerunit  33685  1arithidomlem1  33865  1arithidomlem2  33866  1arithidom  33867  psrmonmul  33980  dimval  34031  dimvalfi  34032  ply1degltdimlem  34052  ply1degltdim  34053  elirng  34116  txomap  34264  locfinreflem  34270  hauseqcn  34328  xpinpreima  34336  xpinpreima2  34337  tpr2rico  34342  mndpluscn  34356  raddcn  34359  xrge0pluscn  34370  xrge0tmdALT  34376  rge0scvg  34379  pl1cn  34385  elzrhunit  34407  qqhf  34416  cnrrext  34440  qqhre  34450  1stmbfm  34691  2ndmbfm  34692  mbfmcnt  34699  omssubadd  34731  carsggect  34749  eulerpartlemsv2  34789  eulerpartlems  34791  eulerpartlemv  34795  eulerpartlemb  34799  eulerpartlemf  34801  eulerpartlemt  34802  eulerpartlemmf  34806  eulerpartlemgvv  34807  eulerpartlemgh  34809  eulerpartlemgs2  34811  sseqmw  34822  sseqf  34823  sseqp1  34826  fiblem  34829  fibp1  34832  signsvtn0  34998  signstres  35003  signshlen  35018  reprinrn  35046  circlemethhgt  35071  txsconnlem  35745  iccllysconn  35755  rellysconn  35756  cvmseu  35781  cvmliftmolem2  35787  cvmliftlem6  35795  cvmliftlem7  35796  cvmliftlem8  35797  cvmliftlem9  35798  cvmliftlem11  35800  cvmliftlem15  35803  cvmlift2lem7  35814  cvmlift2lem10  35817  cvmlift3lem8  35831  cvmlift3lem9  35832  mvrsfpw  36011  mrsubff1  36019  msrid  36050  msrfo  36051  elmsta  36053  mtyf  36057  msubff1  36061  vhmcls  36071  mclsax  36074  elmthm  36081  mthmblem  36085  mclsppslem  36088  iprodefisumlem  36245  fullfunfnv  36451  fullfunfv  36452  tailfb  36921  filnetlem4  36925  regsfromunir1  37084  taupilem3  37996  icoreresf  38031  icoreelrnab  38033  relowlssretop  38042  relowlpssretop  38043  unccur  38287  matunitlindflem1  38300  matunitlindflem2  38301  ptrecube  38304  poimirlem28  38332  poimirlem32  38336  heicant  38339  opnmbllem0  38340  mblfinlem1  38341  mblfinlem2  38342  volsupnfl  38349  cnambfre  38352  dvtan  38354  itg2addnclem  38355  itg2addnclem2  38356  ftc1anclem3  38379  ftc1anclem5  38381  ftc1anclem7  38383  ftc1anclem8  38384  ftc1anc  38385  areacirc  38397  indexdom  38418  sdclem2  38426  sstotbnd2  38458  sstotbnd  38459  isbndx  38466  isbnd3b  38469  prdsbnd  38477  prdstotbnd  38478  ismtyhmeolem  38488  heibor1lem  38493  heiborlem1  38495  heibor  38505  rrnequiv  38519  keridl  38716  ellkr  39896  lkr0f  39901  cdleme50rnlem  41351  aks6d1c2lem4  42927  aks6d1c5  42939  sticksstones11  42956  sticksstones19  42965  sticksstones22  42968  aks6d1c6lem4  42973  aks6d1c6isolem2  42975  fsuppind  43355  elrfirn  43459  ismrcd2  43463  isnacs2  43470  nacsfix  43476  mapfzcons1  43481  mzpcompact2lem  43515  eq0rabdioph  43540  eldioph4b  43571  diophren  43573  pw2f1ocnv  43797  pw2f1o2val2  43800  lmhmfgsplit  43846  pwssplit4  43849  hbt  43890  mpaaeu  43910  mendring  43948  proot1mul  43954  proot1hash  43955  proot1ex  43956  deg1mhm  43960  fgraphopab  43963  hausgraph  43965  nvocnvb  44181  ofsubid  45067  expgrowthi  45076  expgrowth  45078  binomcxplemdvbinom  45096  binomcxplemcvg  45097  binomcxplemnotnn0  45099  relpfrlem  45695  rfcnpre1  45772  rfcnpre2  45784  cncmpmax  45785  rfcnpre3  45786  rfcnpre4  45787  elixpconstg  45840  ffi  45924  islptre  46368  resincncf  46622  dvcosre  46659  dvresntr  46665  volioof  46734  stoweidlem48  46795  fourierdlem12  46866  fourierdlem15  46869  fourierdlem41  46895  fourierdlem42  46896  fourierdlem46  46899  fourierdlem54  46907  fourierdlem56  46909  fourierdlem62  46915  fourierdlem64  46917  fourierdlem65  46918  fourierdlem73  46926  fourierdlem74  46927  fourierdlem75  46928  fourierdlem102  46955  fourierdlem103  46956  fourierdlem104  46957  fourierdlem114  46967  sge0split  47156  elhoi  47289  mbfresmf  47486  cjnpoly  47659  cfsetsnfsetf1  47829  cfsetsnfsetfo  47830  focofob  47850  f1ocof1ob  47851  fafvelcdm  47940  ffnafv  47941  fafv2elcdm  48004  fafv2elrnb  48005  imarnf1pr  48052  2ffzoeq  48098  fundcmpsurbijinjpreimafv  48189  fundcmpsurinjimaid  48193  fargshiftfv  48221  fargshiftf  48222  fargshiftf1  48223  fargshiftfo  48224  cycl3grtri  48745  fdmdifeqresdif  49155  fdivmpt  49353  fdivmptf  49354  refdivmptf  49355  1arymaptf1  49455  2arymaptf1  49466  ackfnnn0  49498  homf0  49820  aacllem  50654  crossp3i  50682