Theorem ffn 6736

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

Syntax hints:   → wi 4   ⊆ wss 3962  ran crn 5689   Fn wfn 6557  ⟶wf 6558

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 6566

This theorem is referenced by:  ffnd  6737  ffun  6739  frel  6741  fdm  6745  ffrn  6749  fresin  6777  fresaun  6779  fresaunres2  6780  fcoi1  6782  feu  6784  f0bi  6791  dffo2  6824  fimadmfo  6829  fdmeu  6964  feqmptdf  6978  fimarab  6982  fvco3  7007  ffvelcdm  7100  dff2  7118  dffo3  7121  dffo4  7122  dffo5  7123  dffo3f  7125  f1ompt  7130  ffnfv  7138  fcdmssb  7141  fcompt  7152  fsn2  7155  fprb  7213  fconst2g  7222  fpr2g  7230  fex  7245  dff13  7274  nvocnv  7300  soisores  7346  fdmexb  7929  fo1stres  8038  fo2ndres  8039  1stcof  8042  2ndcof  8043  curry1f  8129  curry2f  8131  fparlem1  8135  fparlem2  8136  fo2ndf  8144  soseq  8182  tposf2  8273  smo11  8402  fsetexb  8902  mapsnd  8924  pw2f1olem  9114  mapen  9179  mapunen  9184  fissuni  9394  fipreima  9395  indexfi  9397  mapfien  9445  oismo  9577  cantnflt  9709  cantnfp1lem3  9717  cantnflem4  9729  tcrank  9921  updjudhcoinlf  9969  updjudhcoinrg  9970  updjud  9971  infpwfien  10099  cardinfima  10134  dfacacn  10179  cfflb  10296  cofsmo  10306  cfcoflem  10309  coftr  10310  fin23lem40  10388  axdc3lem2  10488  ac6num  10516  ac6c4  10518  ac6s2  10523  ttukeylem6  10551  iunfo  10576  pwcfsdom  10620  fpwwe2lem5  10672  fpwwe2lem7  10674  pwfseqlem3  10697  inar1  10812  tskcard  10818  tskuni  10820  tskurn  10826  gruima  10839  nqerrel  10969  recmulnq  11001  dmrecnq  11005  axpre-sup  11206  ofsubeq0  12260  dfz2  12629  uzn0  12892  rpnnen1lem3  13018  rpnnen1lem5  13020  unirnioo  13485  dfioo2  13486  ioorebas  13487  fseq1p1m1  13634  2ffzeq  13685  fvinim0ffz  13821  injresinjlem  13822  fsequb2  14013  fseqsupcl  14014  fseqsupubi  14015  ser0f  14092  hashgval  14368  hashinf  14370  hashresfn  14375  ffz0hash  14482  fnfzo0hash  14485  wrdred1hash  14595  revlen  14796  revrev  14801  repswlen  14810  repsdf2  14812  cshword  14825  0csh0  14827  lenco  14867  s1co  14868  cshco  14871  swrdco  14872  s7f1o  15001  ofccat  15004  shftf  15114  uzin2  15379  rexanuz  15380  limsuple  15510  limsupval2  15512  rlimres  15590  lo1res  15591  rlimresb  15597  isercolllem2  15698  isercolllem3  15699  isercoll  15700  supcvg  15888  prodf1f  15924  eff2  16131  reeff1  16152  tanval  16160  ruclem4  16266  ruclem12  16273  prmreclem6  16954  1arithlem4  16959  1arith  16960  vdwmc  17011  vdwlem1  17014  vdwlem8  17021  vdwlem13  17026  ramval  17041  0ram  17053  0ram2  17054  0ramcl  17056  ramcl  17062  fsets  17202  firest  17478  0ssc  17887  0subcat  17888  isfull2  17964  arwhoma  18098  gsumval2a  18710  isgrpinv  19023  kerf1ghm  19277  f1omvdconj  19478  pmtrmvd  19488  pmtrfinv  19493  pmtrdifellem4  19511  efgsfo  19771  efgredlem  19779  efgcpbllemb  19787  frgpup3lem  19809  0frgp  19811  gexex  19885  torsubg  19886  gsumval3  19939  gsumzres  19941  gsummptmhm  19972  gsumzoppg  19976  dprdf1o  20066  dprd2db  20077  zrinitorngc  20658  zrtermorngc  20659  zrtermoringc  20691  srngf1o  20865  lmhmima  21063  lmhmpreima  21064  lmhmrnlss  21066  lspextmo  21072  pwssplit1  21075  cnfldadd  21387  cnfldmul  21389  dfcnfldOLD  21397  cnfldplusf  21426  cnfldsub  21427  chrrhm  21563  znunit  21599  psgnevpmb  21622  psgndiflemB  21635  mpofrlmd  21814  frlmipval  21816  frlmphl  21818  frlmlbs  21834  frlmup4  21838  ellspd  21839  lindfmm  21864  lsslindf  21867  psrbaglefi  21963  psrlidm  21999  mplmonmul  22071  evlseu  22124  mpfconst  22142  mpfproj  22143  mpfsubrg  22144  coe1sclmulfv  22301  pf1const  22365  pf1id  22366  pf1subrg  22367  mpfpf1  22370  pf1mpf  22371  mamuass  22421  mamudi  22422  mamudir  22423  mamuvs1  22424  mamuvs2  22425  1mavmul  22569  mavmulass  22570  mdetunilem7  22639  madutpos  22663  lecldbas  23242  lmbr2  23282  cncnpi  23301  cncnp  23303  cnpdis  23316  lmff  23324  pnrmopn  23366  dnsconst  23401  cmpsub  23423  tgcmp  23424  hauscmplem  23429  2ndcctbss  23478  2ndcomap  23481  2ndcsep  23482  1stccnp  23485  kgenidm  23570  iskgen2  23571  1stckgen  23577  kgen2cn  23582  ptpjpre1  23594  pttop  23605  ptuni  23617  ptval2  23624  tx1cn  23632  tx2cn  23633  ptpjcn  23634  ptpjopn  23635  ptclsg  23638  ptcnplem  23644  upxp  23646  txcnmpt  23647  uptx  23648  txcmplem2  23665  txkgen  23675  xkoptsub  23677  xkopt  23678  xkococnlem  23682  xkococn  23683  ptcmpfi  23836  zfbas  23919  uzrest  23920  rnelfmlem  23975  rnelfm  23976  fmfnfmlem2  23978  fmfnfm  23981  lmflf  24028  alexsubALT  24074  clssubg  24132  qustgplem  24144  tsmsres  24167  tsmsxplem1  24176  ucncn  24309  xmettpos  24374  imasdsf1olem  24398  blrnps  24433  blrn  24434  xmeterval  24457  tmslem  24509  tmslemOLD  24510  tmsxms  24514  imasf1oxms  24517  prdsxms  24558  blval2  24590  metuel2  24593  isngp2  24625  isngp3  24626  tngngp2  24688  isnghm  24759  qtopbaslem  24794  qdensere  24805  cnbl0  24809  cnblcld  24810  cnfldms  24811  blssioo  24830  tgioo  24831  tgqioo  24835  xrtgioo  24841  xrsdsre  24845  xrge0tsms  24869  iimulcnOLD  24981  bndth  25003  lebnumlem3  25008  nmhmcn  25166  cphsqrtcl  25231  lmmbr2  25306  caucfil  25330  causs  25345  lmcau  25360  bcth3  25378  cncms  25402  cnfldcusp  25404  rrxmvallem  25451  ivthicc  25506  ovolfioo  25515  ovolficc  25516  ovolficcss  25517  ovollb2lem  25536  ovoliunlem2  25551  ovolshftlem1  25557  ovolicc2  25570  ismbl  25574  voliunlem2  25599  volsup  25604  ioorf  25621  ioorinv  25624  ioorcl  25625  uniiccdif  25626  uniioovol  25627  uniiccvol  25628  uniioombllem2  25631  uniioombllem4  25634  dyaddisj  25644  dyadmax  25646  dyadmbllem  25647  dyadmbl  25648  opnmbllem  25649  opnmblALT  25651  volsup2  25653  mbfdm  25674  mbfima  25678  mbfid  25683  ismbfd  25687  mbfres2  25693  mbfposr  25700  mbfimaopnlem  25703  mbflimsup  25714  0plef  25720  i1f1lem  25737  itg11  25739  itg1addlem4  25747  itg1addlem4OLD  25748  i1fpos  25755  itg1le  25762  itg1climres  25763  mbfi1fseqlem5  25768  mbfi1flimlem  25771  xrge0f  25780  itg2ge0  25784  itg2seq  25791  itg2i1fseqle  25803  itg2i1fseq2  25805  itg2addlem  25807  itg2gt0  25809  limciun  25943  dvres  25960  dvres3a  25963  cpnres  25987  dvfre  26003  dvmptres3  26008  dvlip2  26048  dvgt0lem2  26056  deg1fvi  26138  uc1pmon1p  26205  fta1g  26223  ig1peu  26228  ig1pdvds  26233  plyco0  26245  plypf1  26265  dgrlem  26282  dgrub  26287  dgrlb  26289  coemulc  26308  plyreres  26338  plydivlem3  26351  plydivlem4  26352  plydiveu  26354  plyremlem  26360  fta1lem  26363  fta1  26364  vieta1lem2  26367  plyexmo  26369  elaa  26372  elqaalem3  26377  aannenlem1  26384  pserulm  26479  psercnlem2  26482  psercnlem1  26483  psercn  26484  abelth  26499  reeff1o  26505  pilem1  26509  recosf1o  26591  resinf1o  26592  efif1olem3  26600  efif1olem4  26601  efifo  26603  eff1olem  26604  ellogrn  26615  logcn  26703  dvloglem  26704  logf1o2  26706  efopnlem1  26712  efopnlem2  26713  efopn  26714  logtayl  26716  cxpcn3lem  26804  cxpcn3  26805  resqrtcn  26806  asinneg  26943  areambl  27015  emcllem7  27059  lgamgulm2  27093  basellem4  27141  sqff1o  27239  mpodvdsmulf1o  27251  fsumdvdsmul  27252  dvdsmulf1o  27253  fsumdvdsmulOLD  27254  ostthlem1  27685  ostth  27697  noetasuplem4  27795  madeval2  27906  elold  27922  old1  27928  madeoldsuc  27937  tglnfn  28569  f1otrg  28893  axlowdimlem6  28976  axlowdimlem8  28978  axlowdimlem9  28979  axlowdimlem11  28981  axlowdimlem12  28982  axlowdimlem17  28987  elntg2  29014  crctcshlem4  29849  clwlkclwwlklem2  30028  eucrct2eupth  30273  ex-fpar  30490  cnnvm  30710  sspmlem  30760  nvo00  30789  nmlno0lem  30821  phoeqi  30885  ubthlem1  30898  hhip  31205  hhssabloilem  31289  hhssnv  31292  hhsssh  31297  occllem  31331  shsel  31342  chscllem2  31666  df0op2  31780  hoeq  31788  hocofni  31795  hoaddfni  31798  hosubfni  31799  hon0  31821  ho01i  31856  hoeq1  31858  elnlfn  31956  nmlnop0iALT  32023  lnopco0i  32032  imaelshi  32086  nlelchi  32089  rnbra  32135  cnvbraval  32138  kbass5  32148  hmopidmchi  32179  hmopidmpji  32180  foresf1o  32531  fcomptf  32674  ofpreima  32681  resf1o  32747  maprnin  32748  fpwrelmapffslem  32749  hashgt1  32817  s3clhash  32916  gsumpart  33042  xrge0tsmsd  33047  tocyc01  33120  cyc3evpm  33152  cycpmgcl  33155  cycpmconjslem2  33157  cyc3conja  33159  kerunit  33328  1arithidomlem1  33542  1arithidomlem2  33543  1arithidom  33544  dimval  33627  dimvalfi  33628  ply1degltdimlem  33649  ply1degltdim  33650  elirng  33700  txomap  33794  locfinreflem  33800  hauseqcn  33858  xpinpreima  33866  xpinpreima2  33867  tpr2rico  33872  mndpluscn  33886  raddcn  33889  xrge0pluscn  33900  xrge0tmdALT  33906  rge0scvg  33909  pl1cn  33915  elzrhunit  33939  qqhf  33948  cnrrext  33972  qqhre  33982  indpi1  34000  indpreima  34005  1stmbfm  34241  2ndmbfm  34242  mbfmcnt  34249  omssubadd  34281  carsggect  34299  eulerpartlemsv2  34339  eulerpartlems  34341  eulerpartlemv  34345  eulerpartlemb  34349  eulerpartlemf  34351  eulerpartlemt  34352  eulerpartlemmf  34356  eulerpartlemgvv  34357  eulerpartlemgh  34359  eulerpartlemgs2  34361  sseqmw  34372  sseqf  34373  sseqp1  34376  fiblem  34379  fibp1  34382  plymul02  34539  signsvtn0  34563  signstres  34568  signshlen  34583  reprinrn  34611  circlemethhgt  34636  txsconnlem  35224  iccllysconn  35234  rellysconn  35235  cvmseu  35260  cvmliftmolem2  35266  cvmliftlem6  35274  cvmliftlem7  35275  cvmliftlem8  35276  cvmliftlem9  35277  cvmliftlem11  35279  cvmliftlem15  35282  cvmlift2lem7  35293  cvmlift2lem10  35296  cvmlift3lem8  35310  cvmlift3lem9  35311  mvrsfpw  35490  mrsubff1  35498  msrid  35529  msrfo  35530  elmsta  35532  mtyf  35536  msubff1  35540  vhmcls  35550  mclsax  35553  elmthm  35560  mthmblem  35564  mclsppslem  35567  iprodefisumlem  35719  fullfunfnv  35927  fullfunfv  35928  tailfb  36359  filnetlem4  36363  taupilem3  37301  icoreresf  37334  icoreelrnab  37336  relowlssretop  37345  relowlpssretop  37346  unccur  37589  matunitlindflem1  37602  matunitlindflem2  37603  ptrecube  37606  poimirlem28  37634  poimirlem32  37638  heicant  37641  opnmbllem0  37642  mblfinlem1  37643  mblfinlem2  37644  volsupnfl  37651  cnambfre  37654  dvtan  37656  itg2addnclem  37657  itg2addnclem2  37658  ftc1anclem3  37681  ftc1anclem5  37683  ftc1anclem7  37685  ftc1anclem8  37686  ftc1anc  37687  areacirc  37699  indexdom  37720  sdclem2  37728  sstotbnd2  37760  sstotbnd  37761  isbndx  37768  isbnd3b  37771  prdsbnd  37779  prdstotbnd  37780  ismtyhmeolem  37790  heibor1lem  37795  heiborlem1  37797  heibor  37807  rrnequiv  37821  keridl  38018  ellkr  39070  lkr0f  39075  cdleme50rnlem  40526  aks6d1c2lem4  42108  aks6d1c5  42120  sticksstones11  42137  sticksstones19  42146  sticksstones22  42149  aks6d1c6lem4  42154  aks6d1c6isolem2  42156  fsuppind  42576  elrfirn  42682  ismrcd2  42686  isnacs2  42693  nacsfix  42699  mapfzcons1  42704  mzpcompact2lem  42738  eq0rabdioph  42763  eldioph4b  42798  diophren  42800  pw2f1ocnv  43025  pw2f1o2val2  43028  lmhmfgsplit  43074  pwssplit4  43077  hbt  43118  mpaaeu  43138  mendring  43176  proot1mul  43182  proot1hash  43183  proot1ex  43184  deg1mhm  43188  fgraphopab  43191  hausgraph  43193  nvocnvb  43411  ofsubid  44319  expgrowthi  44328  expgrowth  44330  binomcxplemdvbinom  44348  binomcxplemcvg  44349  binomcxplemnotnn0  44351  rfcnpre1  44956  rfcnpre2  44968  cncmpmax  44969  rfcnpre3  44970  rfcnpre4  44971  elixpconstg  45028  ffi  45115  islptre  45574  resincncf  45830  dvcosre  45867  dvresntr  45873  volioof  45942  stoweidlem48  46003  fourierdlem12  46074  fourierdlem15  46077  fourierdlem41  46103  fourierdlem42  46104  fourierdlem46  46107  fourierdlem48  46109  fourierdlem49  46110  fourierdlem54  46115  fourierdlem56  46117  fourierdlem62  46123  fourierdlem64  46125  fourierdlem65  46126  fourierdlem73  46134  fourierdlem74  46135  fourierdlem75  46136  fourierdlem102  46163  fourierdlem103  46164  fourierdlem104  46165  fourierdlem114  46175  sge0split  46364  elhoi  46497  mbfresmf  46694  cfsetsnfsetf1  47008  cfsetsnfsetfo  47009  focofob  47029  f1ocof1ob  47030  fafvelcdm  47119  ffnafv  47120  fafv2elcdm  47183  fafv2elrnb  47184  imarnf1pr  47231  2ffzoeq  47276  fundcmpsurbijinjpreimafv  47331  fundcmpsurinjimaid  47335  fargshiftfv  47363  fargshiftf  47364  fargshiftf1  47365  fargshiftfo  47366  fdmdifeqresdif  48186  fdivmpt  48389  fdivmptf  48390  refdivmptf  48391  1arymaptf1  48491  2arymaptf1  48502  ackfnnn0  48534  aacllem  49031