Theorem ffn 6739

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

This proof depends on syntax axioms:   → wi 4   ⊆ wss 3900  ran crn 5659   Fn wfn 6561  ⟶wf 6562

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 6570

This theorem is used by:  ffnd  6740  ffun  6742  ffunOLD  6743  frel  6745  fdm  6749  ffrn  6753  fresin  6781  fresaun  6783  fresaunres2  6784  fcoi1  6786  feu  6788  f0bi  6795  dffo2  6830  fimadmfo  6835  fdmeu  6972  feqmptdf  6986  fimarab  6990  fvco3  7016  ffvelcdm  7113  dff2  7131  dffo3  7134  dffo4  7135  dffo5  7136  dffo3f  7138  f1ompt  7143  ffnfv  7151  fcdmssb  7154  fcompt  7166  fsn2  7169  fprb  7230  fconst2g  7240  fpr2g  7248  fex  7263  dff13  7289  nvocnv  7320  soisores  7366  fdmexb  7953  resf1extb  7980  fo1stres  8061  fo2ndres  8062  1stcof  8065  2ndcof  8066  curry1f  8154  curry2f  8156  fparlem1  8160  fparlem2  8161  fo2ndf  8169  soseq  8213  tposf2  8305  smo11  8410  fsetexb  8924  mapsnd  8952  pw2f1olem  9138  mapen  9198  mapunen  9203  fissuni  9384  fipreima  9385  indexfi  9387  mapfien  9437  oismo  9571  cantnflt  9710  cantnfp1lem3  9718  cantnflem4  9730  tcrank  9938  updjudhcoinlf  10050  updjudhcoinrg  10051  updjud  10052  infpwfien  10180  cardinfima  10215  dfacacn  10259  cfflb  10376  cofsmo  10386  cfcoflem  10389  coftr  10390  fin23lem40  10468  axdc3lem2  10568  ac6num  10596  ac6c4  10598  ac6s2  10603  ttukeylem6  10631  iunfo  10662  pwcfsdom  10707  fpwwe2lem5  10759  fpwwe2lem7  10761  pwfseqlem3  10784  inar1  10899  tskcard  10905  tskuni  10907  tskurn  10913  gruima  10926  nqerrel  11056  recmulnq  11088  dmrecnq  11092  axpre-sup  11293  ofsubeq0  12357  indpi1  12374  dfz2  12752  uzn0  13022  rpnnen1lem3  13147  rpnnen1lem5  13149  unirnioo  13620  dfioo2  13621  ioorebas  13622  fseq1p1m1  13772  2ffzeq  13823  fvinim0ffz  13964  injresinjlem  13965  fsequb2  14159  fseqsupcl  14160  fseqsupubi  14161  ser0f  14238  hashgval  14518  hashinf  14520  hashresfn  14525  ffz0hash  14633  fnfzo0hash  14636  wrdred1hash  14747  revlen  14953  revrev  14958  repswlen  14969  repsdf2  14971  cshword  14984  0csh0  14986  lenco  15025  s1co  15026  cshco  15029  swrdco  15030  s7f1o  15162  ofccat  15165  shftf  15275  uzin2  15556  rexanuz  15557  limsuple  15689  limsupval2  15691  rlimres  15769  lo1res  15770  rlimresb  15776  isercolllem2  15877  isercolllem3  15878  isercoll  15879  supcvg  16069  prodf1f  16105  eff2  16311  reeff1  16332  tanval  16340  ruclem4  16446  ruclem12  16453  prmreclem6  17143  1arithlem4  17148  1arith  17149  vdwmc  17200  vdwlem1  17203  vdwlem8  17210  vdwlem13  17215  ramval  17230  0ram  17242  0ram2  17243  0ramcl  17245  ramcl  17251  fsets  17391  firest  17653  0ssc  18062  0subcat  18063  isfull2  18138  arwhoma  18270  gsumval2a  18924  isgrpinv  19254  kerf1ghm  19511  f1omvdconj  19711  pmtrmvd  19721  pmtrfinv  19726  pmtrdifellem4  19744  efgsfo  20004  efgredlem  20012  efgcpbllemb  20020  frgpup3lem  20042  0frgp  20044  gexex  20118  torsubg  20119  gsumval3  20172  gsumzres  20174  gsummptmhm  20205  gsumzoppg  20209  dprdf1o  20299  dprd2db  20310  zrinitorngc  20945  zrtermorngc  20946  zrtermoringc  20978  srngf1o  21156  lmhmima  21373  lmhmpreima  21374  lmhmrnlss  21376  lspextmo  21382  pwssplit1  21385  cnfldadd  21735  cnfldmul  21737  cnfldplusf  21757  cnfldsub  21758  chrrhm  21892  znunit  21924  psgnevpmb  21948  psgndiflemB  21961  mpofrlmd  22138  frlmipval  22140  frlmphl  22142  frlmlbs  22158  frlmup4  22162  ellspd  22163  lindfmm  22188  lsslindf  22191  psrbaglefi  22289  psrlidm  22324  mplmonmul  22400  evlseu  22447  mpfconst  22473  mpfproj  22474  mpfsubrg  22475  coe1sclmulfv  22657  pf1const  22719  pf1id  22720  pf1subrg  22721  mpfpf1  22724  pf1mpf  22725  mamuass  22772  mamudi  22773  mamudir  22774  mamuvs1  22775  mamuvs2  22776  1mavmul  22918  mavmulass  22919  mdetunilem7  22988  madutpos  23012  matunitlindflem1  23049  matunitlindflem2  23050  lecldbas  23592  lmbr2  23632  cncnpi  23651  cncnp  23653  cnpdis  23666  lmff  23674  pnrmopn  23716  dnsconst  23751  cmpsub  23773  tgcmp  23774  hauscmplem  23779  2ndcctbss  23829  2ndcomap  23832  2ndcsep  23833  1stccnp  23836  kgenidm  23921  iskgen2  23922  1stckgen  23928  kgen2cn  23933  ptpjpre1  23945  pttop  23956  ptuni  23968  ptval2  23975  tx1cn  23983  tx2cn  23984  ptpjcn  23985  ptpjopn  23986  ptclsg  23989  ptcnplem  23995  upxp  23997  txcnmpt  23998  uptx  23999  txcmplem2  24016  txkgen  24026  xkoptsub  24028  xkopt  24029  xkococnlem  24033  xkococn  24034  ptcmpfi  24187  zfbas  24270  uzrest  24271  rnelfmlem  24326  rnelfm  24327  fmfnfmlem2  24329  fmfnfm  24332  lmflf  24379  alexsubALT  24425  clssubg  24483  qustgplem  24495  tsmsres  24518  tsmsxplem1  24527  ucncn  24658  xmettpos  24723  imasdsf1olem  24747  blrnps  24782  blrn  24783  xmeterval  24806  tmslem  24856  tmsxms  24860  imasf1oxms  24863  prdsxms  24904  blval2  24936  metuel2  24939  isngp2  24971  isngp3  24972  tngngp2  25026  isnghm  25097  qtopbaslem  25132  qdensere  25143  cnbl0  25147  cnblcld  25148  cnfldms  25149  blssioo  25169  tgioo  25170  tgqioo  25174  xrtgioo  25181  xrsdsre  25185  xrge0tsms  25209  bndth  25334  lebnumlem3  25339  nmhmcn  25496  cphsqrtcl  25560  lmmbr2  25635  caucfil  25659  causs  25674  lmcau  25689  bcth3  25707  cncms  25731  cnfldcusp  25733  rrxmvallem  25780  ivthicc  25834  ovolfioo  25843  ovolficc  25844  ovolficcss  25845  ovollb2lem  25864  ovoliunlem2  25879  ovolshftlem1  25885  ovolicc2  25898  ismbl  25902  voliunlem2  25927  volsup  25932  ioorf  25949  ioorinv  25952  ioorcl  25953  uniiccdif  25954  uniioovol  25955  uniiccvol  25956  uniioombllem2  25959  uniioombllem4  25962  dyaddisj  25972  dyadmax  25974  dyadmbllem  25975  dyadmbl  25976  opnmbllem  25977  opnmblALT  25979  volsup2  25981  mbfdm  26002  mbfima  26006  mbfid  26011  ismbfd  26015  mbfres2  26021  mbfposr  26028  mbfimaopnlem  26031  mbflimsup  26042  0plef  26048  i1f1lem  26065  itg11  26067  itg1addlem4  26075  i1fpos  26082  itg1le  26089  itg1climres  26090  mbfi1fseqlem5  26095  mbfi1flimlem  26098  xrge0f  26107  itg2ge0  26111  itg2seq  26118  itg2i1fseqle  26130  itg2i1fseq2  26132  itg2addlem  26134  itg2gt0  26136  limciun  26269  dvres  26286  dvres3a  26289  cpnres  26312  dvfre  26326  dvmptres3  26331  dvlip2  26370  dvgt0lem2  26378  deg1fvi  26458  uc1pmon1p  26525  fta1g  26543  ig1peu  26548  ig1pdvds  26553  plyco0  26565  plypf1  26586  dgrlem  26603  dgrub  26608  dgrlb  26610  coemulc  26629  plymul02  26656  plyreres  26659  plydivlem3  26671  plydivlem4  26672  plydiveu  26674  plyremlem  26680  fta1lem  26683  fta1  26684  vieta1lem2  26689  plyexmo  26691  elaa  26696  elqaalem3  26701  aannenlem1  26712  pserulm  26806  psercnlem2  26808  psercnlem1  26809  psercn  26810  abelth  26825  reeff1o  26831  pilem1  26835  recosf1o  26920  resinf1o  26921  efif1olem3  26929  efif1olem4  26930  efifo  26932  eff1olem  26933  ellogrn  26944  logcn  27032  dvloglem  27033  logf1o2  27035  efopnlem1  27041  efopnlem2  27042  efopn  27043  logtayl  27045  cxpcn3lem  27132  cxpcn3  27133  resqrtcn  27134  asinneg  27271  areambl  27343  emcllem7  27386  lgamgulm2  27420  basellem4  27468  sqff1o  27566  mpodvdsmulf1o  27578  fsumdvdsmul  27579  dvdsmulf1o  27580  ostthlem1  28011  ostth  28023  noetasuplem4  28150  madeval2  28276  elold  28302  old1  28308  madeoldsuc  28328  tglnfn  29067  tgplnfn  29310  f1otrg  29505  axlowdimlem6  29582  axlowdimlem8  29584  axlowdimlem9  29585  axlowdimlem11  29587  axlowdimlem12  29588  axlowdimlem17  29593  elntg2  29620  dfpth2  30371  cyclnumvtx  30445  crctcshlem4  30466  clwlkclwwlklem2  30648  eucrct2eupth  30903  ex-fpar  31120  cnnvm  31341  sspmlem  31391  nvo00  31420  nmlno0lem  31452  phoeqi  31516  ubthlem1  31529  hhip  31836  hhssabloilem  31920  hhssnv  31923  hhsssh  31928  occllem  31962  shsel  31973  chscllem2  32297  df0op2  32411  hoeq  32419  hocofni  32426  hoaddfni  32429  hosubfni  32430  hon0  32452  ho01i  32487  hoeq1  32489  elnlfn  32587  nmlnop0iALT  32654  lnopco0i  32663  imaelshi  32717  nlelchi  32720  rnbra  32766  cnvbraval  32769  kbass5  32779  hmopidmchi  32810  hmopidmpji  32811  foresf1o  33199  fcomptf  33350  ofpreima  33357  resf1o  33418  maprnin  33419  fpwrelmapffslem  33420  hashgt1  33496  indpreima  33528  s3clhash  33608  gsumpart  33723  xrge0tsmsd  33733  tocyc01  33778  cyc3evpm  33810  cycpmgcl  33813  cycpmconjslem2  33815  cyc3conja  33817  kerunit  33990  1arithidomlem1  34171  1arithidomlem2  34172  1arithidom  34173  psrmonmul  34293  dimval  34344  dimvalfi  34345  ply1degltdimlem  34365  ply1degltdim  34366  elirng  34429  txomap  34577  locfinreflem  34583  hauseqcn  34641  xpinpreima  34649  xpinpreima2  34650  tpr2rico  34655  mndpluscn  34669  raddcn  34672  xrge0pluscn  34683  xrge0tmdALT  34689  rge0scvg  34692  pl1cn  34698  elzrhunit  34720  qqhf  34729  cnrrext  34753  qqhre  34763  1stmbfm  35003  2ndmbfm  35004  mbfmcnt  35011  omssubadd  35043  carsggect  35061  eulerpartlemsv2  35101  eulerpartlems  35103  eulerpartlemv  35107  eulerpartlemb  35111  eulerpartlemf  35113  eulerpartlemt  35114  eulerpartlemmf  35118  eulerpartlemgvv  35119  eulerpartlemgh  35121  eulerpartlemgs2  35123  sseqmw  35134  sseqf  35135  sseqp1  35138  fiblem  35141  fibp1  35144  signsvtn0  35310  signstres  35315  signshlen  35330  reprinrn  35358  circlemethhgt  35383  ptpconn  36206  txsconnlem  36213  iccllysconn  36223  rellysconn  36224  cvmseu  36249  cvmliftmolem2  36255  cvmliftlem6  36263  cvmliftlem7  36264  cvmliftlem8  36265  cvmliftlem9  36266  cvmliftlem11  36268  cvmliftlem15  36271  cvmlift2lem7  36282  cvmlift2lem10  36285  cvmlift3lem8  36299  cvmlift3lem9  36300  mvrsfpw  36479  mrsubff1  36487  msrid  36518  msrfo  36519  elmsta  36521  mtyf  36525  msubff1  36529  vhmcls  36539  mclsax  36542  elmthm  36549  mthmblem  36553  mclsppslem  36556  iprodefisumlem  36720  fullfunfnv  36925  fullfunfv  36926  tailfb  37380  filnetlem4  37384  regsfromunir1  37543  nvo3  38230  taupilem3  38508  icoreresf  38543  icoreelrnab  38545  relowlssretop  38554  relowlpssretop  38555  unccur  38794  ptrecube  38806  poimirlem28  38834  poimirlem32  38838  heicant  38841  opnmbllem0  38842  mblfinlem1  38843  mblfinlem2  38844  volsupnfl  38851  cnambfre  38854  dvtan  38856  itg2addnclem  38857  itg2addnclem2  38858  ftc1anclem3  38881  ftc1anclem5  38883  ftc1anclem7  38885  ftc1anclem8  38886  ftc1anc  38887  areacirc  38899  indexdom  38936  sdclem2  38942  sstotbnd2  38974  sstotbnd  38975  isbndx  38982  isbnd3b  38985  prdsbnd  38993  prdstotbnd  38994  ismtyhmeolem  39004  heibor1lem  39009  heiborlem1  39011  heibor  39021  rrnequiv  39035  keridl  39232  ellkr  40412  lkr0f  40417  cdleme50rnlem  41867  aks6d1c2lem4  43443  aks6d1c5  43455  sticksstones11  43472  sticksstones19  43481  sticksstones22  43484  aks6d1c6lem4  43489  aks6d1c6isolem2  43491  fsuppind  43884  elrfirn  43972  ismrcd2  43976  isnacs2  43983  nacsfix  43989  mapfzcons1  43994  mzpcompact2lem  44028  eq0rabdioph  44053  eldioph4b  44084  diophren  44086  pw2f1ocnv  44310  pw2f1o2val2  44313  lmhmfgsplit  44354  pwssplit4  44357  hbt  44397  mpaaeu  44417  mendring  44451  proot1mul  44457  proot1hash  44458  proot1ex  44459  deg1mhm  44463  fgraphopab  44466  hausgraph  44468  nvocnvb  44684  ofsubid  45569  expgrowthi  45578  expgrowth  45580  binomcxplemdvbinom  45598  binomcxplemcvg  45599  binomcxplemnotnn0  45601  relpfrlem  46207  rfcnpre1  46310  rfcnpre2  46322  cncmpmax  46323  rfcnpre3  46324  rfcnpre4  46325  elixpconstg  46377  ffi  46461  islptre  46904  resincncf  47158  dvcosre  47195  dvresntr  47201  volioof  47270  stoweidlem48  47331  fourierdlem12  47402  fourierdlem15  47405  fourierdlem41  47431  fourierdlem42  47432  fourierdlem46  47435  fourierdlem54  47443  fourierdlem56  47445  fourierdlem62  47451  fourierdlem64  47453  fourierdlem65  47454  fourierdlem73  47462  fourierdlem74  47463  fourierdlem75  47464  fourierdlem102  47491  fourierdlem103  47492  fourierdlem104  47493  fourierdlem114  47503  sge0split  47692  elhoi  47825  mbfresmf  48022  cjnpoly  48212  cfsetsnfsetf1  48402  cfsetsnfsetfo  48403  focofob  48423  f1ocof1ob  48424  fafvelcdm  48513  ffnafv  48514  fafv2elcdm  48577  fafv2elrnb  48578  imarnf1pr  48625  2ffzoeq  48671  fundcmpsurbijinjpreimafv  48762  fundcmpsurinjimaid  48766  fargshiftfv  48794  fargshiftf  48795  fargshiftf1  48796  fargshiftfo  48797  cycl3grtri  49318  fdmdifeqresdif  49785  fdivmpt  49983  fdivmptf  49984  refdivmptf  49985  1arymaptf1  50085  2arymaptf1  50096  ackfnnn0  50128  homf0  50454  tanhval  51247  tanhf  51249  tanhcl  51250  aacllem  51367