Theorem ffn 6688

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

Syntax hints:   → wi 4   ⊆ wss 3914  ran crn 5639   Fn wfn 6506  ⟶wf 6507

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 6515

This theorem is referenced by:  ffnd  6689  ffun  6691  frel  6693  fdm  6697  ffrn  6701  fresin  6729  fresaun  6731  fresaunres2  6732  fcoi1  6734  feu  6736  f0bi  6743  dffo2  6776  fimadmfo  6781  fdmeu  6917  feqmptdf  6931  fimarab  6935  fvco3  6960  ffvelcdm  7053  dff2  7071  dffo3  7074  dffo4  7075  dffo5  7076  dffo3f  7078  f1ompt  7083  ffnfv  7091  fcdmssb  7094  fcompt  7105  fsn2  7108  fprb  7168  fconst2g  7177  fpr2g  7185  fex  7200  dff13  7229  nvocnv  7256  soisores  7302  fdmexb  7883  resf1extb  7910  fo1stres  7994  fo2ndres  7995  1stcof  7998  2ndcof  7999  curry1f  8085  curry2f  8087  fparlem1  8091  fparlem2  8092  fo2ndf  8100  soseq  8138  tposf2  8229  smo11  8333  fsetexb  8837  mapsnd  8859  pw2f1olem  9045  mapen  9105  mapunen  9110  fissuni  9308  fipreima  9309  indexfi  9311  mapfien  9359  oismo  9493  cantnflt  9625  cantnfp1lem3  9633  cantnflem4  9645  tcrank  9837  updjudhcoinlf  9885  updjudhcoinrg  9886  updjud  9887  infpwfien  10015  cardinfima  10050  dfacacn  10095  cfflb  10212  cofsmo  10222  cfcoflem  10225  coftr  10226  fin23lem40  10304  axdc3lem2  10404  ac6num  10432  ac6c4  10434  ac6s2  10439  ttukeylem6  10467  iunfo  10492  pwcfsdom  10536  fpwwe2lem5  10588  fpwwe2lem7  10590  pwfseqlem3  10613  inar1  10728  tskcard  10734  tskuni  10736  tskurn  10742  gruima  10755  nqerrel  10885  recmulnq  10917  dmrecnq  10921  axpre-sup  11122  ofsubeq0  12183  dfz2  12548  uzn0  12810  rpnnen1lem3  12938  rpnnen1lem5  12940  unirnioo  13410  dfioo2  13411  ioorebas  13412  fseq1p1m1  13559  2ffzeq  13610  fvinim0ffz  13747  injresinjlem  13748  fsequb2  13941  fseqsupcl  13942  fseqsupubi  13943  ser0f  14020  hashgval  14298  hashinf  14300  hashresfn  14305  ffz0hash  14412  fnfzo0hash  14415  wrdred1hash  14526  revlen  14727  revrev  14732  repswlen  14741  repsdf2  14743  cshword  14756  0csh0  14758  lenco  14798  s1co  14799  cshco  14802  swrdco  14803  s7f1o  14932  ofccat  14935  shftf  15045  uzin2  15311  rexanuz  15312  limsuple  15444  limsupval2  15446  rlimres  15524  lo1res  15525  rlimresb  15531  isercolllem2  15632  isercolllem3  15633  isercoll  15634  supcvg  15822  prodf1f  15858  eff2  16067  reeff1  16088  tanval  16096  ruclem4  16202  ruclem12  16209  prmreclem6  16892  1arithlem4  16897  1arith  16898  vdwmc  16949  vdwlem1  16952  vdwlem8  16959  vdwlem13  16964  ramval  16979  0ram  16991  0ram2  16992  0ramcl  16994  ramcl  17000  fsets  17139  firest  17395  0ssc  17799  0subcat  17800  isfull2  17875  arwhoma  18007  gsumval2a  18612  isgrpinv  18925  kerf1ghm  19179  f1omvdconj  19376  pmtrmvd  19386  pmtrfinv  19391  pmtrdifellem4  19409  efgsfo  19669  efgredlem  19677  efgcpbllemb  19685  frgpup3lem  19707  0frgp  19709  gexex  19783  torsubg  19784  gsumval3  19837  gsumzres  19839  gsummptmhm  19870  gsumzoppg  19874  dprdf1o  19964  dprd2db  19975  zrinitorngc  20551  zrtermorngc  20552  zrtermoringc  20584  srngf1o  20757  lmhmima  20954  lmhmpreima  20955  lmhmrnlss  20957  lspextmo  20963  pwssplit1  20966  cnfldadd  21270  cnfldmul  21272  dfcnfldOLD  21280  cnfldplusf  21308  cnfldsub  21309  chrrhm  21441  znunit  21473  psgnevpmb  21496  psgndiflemB  21509  mpofrlmd  21686  frlmipval  21688  frlmphl  21690  frlmlbs  21706  frlmup4  21710  ellspd  21711  lindfmm  21736  lsslindf  21739  psrbaglefi  21835  psrlidm  21871  mplmonmul  21943  evlseu  21990  mpfconst  22008  mpfproj  22009  mpfsubrg  22010  coe1sclmulfv  22169  pf1const  22233  pf1id  22234  pf1subrg  22235  mpfpf1  22238  pf1mpf  22239  mamuass  22289  mamudi  22290  mamudir  22291  mamuvs1  22292  mamuvs2  22293  1mavmul  22435  mavmulass  22436  mdetunilem7  22505  madutpos  22529  lecldbas  23106  lmbr2  23146  cncnpi  23165  cncnp  23167  cnpdis  23180  lmff  23188  pnrmopn  23230  dnsconst  23265  cmpsub  23287  tgcmp  23288  hauscmplem  23293  2ndcctbss  23342  2ndcomap  23345  2ndcsep  23346  1stccnp  23349  kgenidm  23434  iskgen2  23435  1stckgen  23441  kgen2cn  23446  ptpjpre1  23458  pttop  23469  ptuni  23481  ptval2  23488  tx1cn  23496  tx2cn  23497  ptpjcn  23498  ptpjopn  23499  ptclsg  23502  ptcnplem  23508  upxp  23510  txcnmpt  23511  uptx  23512  txcmplem2  23529  txkgen  23539  xkoptsub  23541  xkopt  23542  xkococnlem  23546  xkococn  23547  ptcmpfi  23700  zfbas  23783  uzrest  23784  rnelfmlem  23839  rnelfm  23840  fmfnfmlem2  23842  fmfnfm  23845  lmflf  23892  alexsubALT  23938  clssubg  23996  qustgplem  24008  tsmsres  24031  tsmsxplem1  24040  ucncn  24172  xmettpos  24237  imasdsf1olem  24261  blrnps  24296  blrn  24297  xmeterval  24320  tmslem  24370  tmsxms  24374  imasf1oxms  24377  prdsxms  24418  blval2  24450  metuel2  24453  isngp2  24485  isngp3  24486  tngngp2  24540  isnghm  24611  qtopbaslem  24646  qdensere  24657  cnbl0  24661  cnblcld  24662  cnfldms  24663  blssioo  24683  tgioo  24684  tgqioo  24688  xrtgioo  24695  xrsdsre  24699  xrge0tsms  24723  iimulcnOLD  24835  bndth  24857  lebnumlem3  24862  nmhmcn  25020  cphsqrtcl  25084  lmmbr2  25159  caucfil  25183  causs  25198  lmcau  25213  bcth3  25231  cncms  25255  cnfldcusp  25257  rrxmvallem  25304  ivthicc  25359  ovolfioo  25368  ovolficc  25369  ovolficcss  25370  ovollb2lem  25389  ovoliunlem2  25404  ovolshftlem1  25410  ovolicc2  25423  ismbl  25427  voliunlem2  25452  volsup  25457  ioorf  25474  ioorinv  25477  ioorcl  25478  uniiccdif  25479  uniioovol  25480  uniiccvol  25481  uniioombllem2  25484  uniioombllem4  25487  dyaddisj  25497  dyadmax  25499  dyadmbllem  25500  dyadmbl  25501  opnmbllem  25502  opnmblALT  25504  volsup2  25506  mbfdm  25527  mbfima  25531  mbfid  25536  ismbfd  25540  mbfres2  25546  mbfposr  25553  mbfimaopnlem  25556  mbflimsup  25567  0plef  25573  i1f1lem  25590  itg11  25592  itg1addlem4  25600  i1fpos  25607  itg1le  25614  itg1climres  25615  mbfi1fseqlem5  25620  mbfi1flimlem  25623  xrge0f  25632  itg2ge0  25636  itg2seq  25643  itg2i1fseqle  25655  itg2i1fseq2  25657  itg2addlem  25659  itg2gt0  25661  limciun  25795  dvres  25812  dvres3a  25815  cpnres  25839  dvfre  25855  dvmptres3  25860  dvlip2  25900  dvgt0lem2  25908  deg1fvi  25990  uc1pmon1p  26057  fta1g  26075  ig1peu  26080  ig1pdvds  26085  plyco0  26097  plypf1  26117  dgrlem  26134  dgrub  26139  dgrlb  26141  coemulc  26160  plyreres  26190  plydivlem3  26203  plydivlem4  26204  plydiveu  26206  plyremlem  26212  fta1lem  26215  fta1  26216  vieta1lem2  26219  plyexmo  26221  elaa  26224  elqaalem3  26229  aannenlem1  26236  pserulm  26331  psercnlem2  26334  psercnlem1  26335  psercn  26336  abelth  26351  reeff1o  26357  pilem1  26361  recosf1o  26444  resinf1o  26445  efif1olem3  26453  efif1olem4  26454  efifo  26456  eff1olem  26457  ellogrn  26468  logcn  26556  dvloglem  26557  logf1o2  26559  efopnlem1  26565  efopnlem2  26566  efopn  26567  logtayl  26569  cxpcn3lem  26657  cxpcn3  26658  resqrtcn  26659  asinneg  26796  areambl  26868  emcllem7  26912  lgamgulm2  26946  basellem4  26994  sqff1o  27092  mpodvdsmulf1o  27104  fsumdvdsmul  27105  dvdsmulf1o  27106  fsumdvdsmulOLD  27107  ostthlem1  27538  ostth  27550  noetasuplem4  27648  madeval2  27761  elold  27781  old1  27787  madeoldsuc  27796  tglnfn  28474  f1otrg  28798  axlowdimlem6  28874  axlowdimlem8  28876  axlowdimlem9  28877  axlowdimlem11  28879  axlowdimlem12  28880  axlowdimlem17  28885  elntg2  28912  dfpth2  29659  cyclnumvtx  29730  crctcshlem4  29750  clwlkclwwlklem2  29929  eucrct2eupth  30174  ex-fpar  30391  cnnvm  30611  sspmlem  30661  nvo00  30690  nmlno0lem  30722  phoeqi  30786  ubthlem1  30799  hhip  31106  hhssabloilem  31190  hhssnv  31193  hhsssh  31198  occllem  31232  shsel  31243  chscllem2  31567  df0op2  31681  hoeq  31689  hocofni  31696  hoaddfni  31699  hosubfni  31700  hon0  31722  ho01i  31757  hoeq1  31759  elnlfn  31857  nmlnop0iALT  31924  lnopco0i  31933  imaelshi  31987  nlelchi  31990  rnbra  32036  cnvbraval  32039  kbass5  32049  hmopidmchi  32080  hmopidmpji  32081  foresf1o  32433  fcomptf  32582  ofpreima  32589  resf1o  32653  maprnin  32654  fpwrelmapffslem  32655  hashgt1  32733  indpi1  32783  indpreima  32788  s3clhash  32869  gsumpart  32997  xrge0tsmsd  33002  tocyc01  33075  cyc3evpm  33107  cycpmgcl  33110  cycpmconjslem2  33112  cyc3conja  33114  kerunit  33297  1arithidomlem1  33506  1arithidomlem2  33507  1arithidom  33508  dimval  33596  dimvalfi  33597  ply1degltdimlem  33618  ply1degltdim  33619  elirng  33681  txomap  33824  locfinreflem  33830  hauseqcn  33888  xpinpreima  33896  xpinpreima2  33897  tpr2rico  33902  mndpluscn  33916  raddcn  33919  xrge0pluscn  33930  xrge0tmdALT  33936  rge0scvg  33939  pl1cn  33945  elzrhunit  33967  qqhf  33976  cnrrext  34000  qqhre  34010  1stmbfm  34251  2ndmbfm  34252  mbfmcnt  34259  omssubadd  34291  carsggect  34309  eulerpartlemsv2  34349  eulerpartlems  34351  eulerpartlemv  34355  eulerpartlemb  34359  eulerpartlemf  34361  eulerpartlemt  34362  eulerpartlemmf  34366  eulerpartlemgvv  34367  eulerpartlemgh  34369  eulerpartlemgs2  34371  sseqmw  34382  sseqf  34383  sseqp1  34386  fiblem  34389  fibp1  34392  plymul02  34537  signsvtn0  34561  signstres  34566  signshlen  34581  reprinrn  34609  circlemethhgt  34634  txsconnlem  35227  iccllysconn  35237  rellysconn  35238  cvmseu  35263  cvmliftmolem2  35269  cvmliftlem6  35277  cvmliftlem7  35278  cvmliftlem8  35279  cvmliftlem9  35280  cvmliftlem11  35282  cvmliftlem15  35285  cvmlift2lem7  35296  cvmlift2lem10  35299  cvmlift3lem8  35313  cvmlift3lem9  35314  mvrsfpw  35493  mrsubff1  35501  msrid  35532  msrfo  35533  elmsta  35535  mtyf  35539  msubff1  35543  vhmcls  35553  mclsax  35556  elmthm  35563  mthmblem  35567  mclsppslem  35570  iprodefisumlem  35727  fullfunfnv  35934  fullfunfv  35935  tailfb  36365  filnetlem4  36369  taupilem3  37307  icoreresf  37340  icoreelrnab  37342  relowlssretop  37351  relowlpssretop  37352  unccur  37597  matunitlindflem1  37610  matunitlindflem2  37611  ptrecube  37614  poimirlem28  37642  poimirlem32  37646  heicant  37649  opnmbllem0  37650  mblfinlem1  37651  mblfinlem2  37652  volsupnfl  37659  cnambfre  37662  dvtan  37664  itg2addnclem  37665  itg2addnclem2  37666  ftc1anclem3  37689  ftc1anclem5  37691  ftc1anclem7  37693  ftc1anclem8  37694  ftc1anc  37695  areacirc  37707  indexdom  37728  sdclem2  37736  sstotbnd2  37768  sstotbnd  37769  isbndx  37776  isbnd3b  37779  prdsbnd  37787  prdstotbnd  37788  ismtyhmeolem  37798  heibor1lem  37803  heiborlem1  37805  heibor  37815  rrnequiv  37829  keridl  38026  ellkr  39082  lkr0f  39087  cdleme50rnlem  40538  aks6d1c2lem4  42115  aks6d1c5  42127  sticksstones11  42144  sticksstones19  42153  sticksstones22  42156  aks6d1c6lem4  42161  aks6d1c6isolem2  42163  fsuppind  42578  elrfirn  42683  ismrcd2  42687  isnacs2  42694  nacsfix  42700  mapfzcons1  42705  mzpcompact2lem  42739  eq0rabdioph  42764  eldioph4b  42799  diophren  42801  pw2f1ocnv  43026  pw2f1o2val2  43029  lmhmfgsplit  43075  pwssplit4  43078  hbt  43119  mpaaeu  43139  mendring  43177  proot1mul  43183  proot1hash  43184  proot1ex  43185  deg1mhm  43189  fgraphopab  43192  hausgraph  43194  nvocnvb  43411  ofsubid  44313  expgrowthi  44322  expgrowth  44324  binomcxplemdvbinom  44342  binomcxplemcvg  44343  binomcxplemnotnn0  44345  relpfrlem  44943  rfcnpre1  45013  rfcnpre2  45025  cncmpmax  45026  rfcnpre3  45027  rfcnpre4  45028  elixpconstg  45083  ffi  45167  islptre  45617  resincncf  45873  dvcosre  45910  dvresntr  45916  volioof  45985  stoweidlem48  46046  fourierdlem12  46117  fourierdlem15  46120  fourierdlem41  46146  fourierdlem42  46147  fourierdlem46  46150  fourierdlem48  46152  fourierdlem49  46153  fourierdlem54  46158  fourierdlem56  46160  fourierdlem62  46166  fourierdlem64  46168  fourierdlem65  46169  fourierdlem73  46177  fourierdlem74  46178  fourierdlem75  46179  fourierdlem102  46206  fourierdlem103  46207  fourierdlem104  46208  fourierdlem114  46218  sge0split  46407  elhoi  46540  mbfresmf  46737  cjnpoly  46890  cfsetsnfsetf1  47060  cfsetsnfsetfo  47061  focofob  47081  f1ocof1ob  47082  fafvelcdm  47171  ffnafv  47172  fafv2elcdm  47235  fafv2elrnb  47236  imarnf1pr  47283  2ffzoeq  47328  fundcmpsurbijinjpreimafv  47408  fundcmpsurinjimaid  47412  fargshiftfv  47440  fargshiftf  47441  fargshiftf1  47442  fargshiftfo  47443  cycl3grtri  47946  fdmdifeqresdif  48330  fdivmpt  48529  fdivmptf  48530  refdivmptf  48531  1arymaptf1  48631  2arymaptf1  48642  ackfnnn0  48674  homf0  48998  aacllem  49790