MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  fnfun Structured version   Visualization version   GIF version

Theorem fnfun 6026
Description: A function with domain is a function. (Contributed by NM, 1-Aug-1994.)
Assertion
Ref Expression
fnfun (𝐹 Fn 𝐴 → Fun 𝐹)

Proof of Theorem fnfun
StepHypRef Expression
1 df-fn 5929 . 2 (𝐹 Fn 𝐴 ↔ (Fun 𝐹 ∧ dom 𝐹 = 𝐴))
21simplbi 475 1 (𝐹 Fn 𝐴 → Fun 𝐹)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1523  dom cdm 5143  Fun wfun 5920   Fn wfn 5921
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 197  df-an 385  df-fn 5929
This theorem is referenced by:  fnrel  6027  funfni  6029  fnco  6037  fnssresb  6041  ffun  6086  f1fun  6141  f1ofun  6177  fnbrfvb  6274  fvelimab  6292  fvun1  6308  elpreima  6377  respreima  6384  fnsnr  6472  fnprb  6513  fntpb  6514  fconst3  6518  fnfvima  6536  fnunirn  6551  nvof1o  6576  f1eqcocnv  6596  fnexALT  7174  curry1  7314  curry2  7317  suppvalfn  7347  suppfnss  7365  fnsuppres  7367  wfrlem2  7460  wfrlem14  7473  tfrlem4  7520  tfrlem5  7521  tfrlem11  7529  tz7.48-2  7582  tz7.49  7585  fndmeng  8075  fnfi  8279  fodomfi  8280  resfnfinfin  8287  fczfsuppd  8334  marypha2lem4  8385  inf0  8556  r1elss  8707  dfac8alem  8890  alephfp  8969  dfac3  8982  dfac9  8996  dfac12lem1  9003  dfac12lem2  9004  r1om  9104  cfsmolem  9130  alephsing  9136  zorn2lem1  9356  zorn2lem5  9360  zorn2lem6  9361  zorn2lem7  9362  ttukeylem3  9371  ttukeylem6  9374  fnct  9397  smobeth  9446  fpwwe2lem9  9498  wunr1om  9579  tskr1om  9627  tskr1om2  9628  uzrdg0i  12798  uzrdgsuci  12799  hashkf  13159  cshimadifsn  13621  cshimadifsn0  13622  shftfn  13857  phimullem  15531  imasaddvallem  16236  imasvscaval  16245  frmdss2  17447  lcomfsupp  18951  lidlval  19240  rspval  19241  psrbagev1  19558  psgnghm  19974  frlmsslsp  20183  iscldtop  20947  2ndcomap  21309  qtoptop  21551  basqtop  21562  qtoprest  21568  kqfvima  21581  isr0  21588  kqreglem1  21592  kqnrmlem1  21594  kqnrmlem2  21595  elrnust  22075  ustbas  22078  uniiccdif  23392  fcoinver  29544  mdetpmtr1  30017  fimaproj  30028  sseqf  30582  sseqfv2  30584  elorrvc  30653  bnj930  30966  bnj1371  31223  bnj1497  31254  frrlem2  31906  noextendseq  31945  madeval  32060  filnetlem4  32501  heibor1lem  33738  diaf11N  36655  dibf11N  36767  dibclN  36768  dihintcl  36950  ismrc  37581  dnnumch1  37931  aomclem4  37944  aomclem6  37946  ntrclsfv1  38670  ntrneifv1  38694  fvelimad  39772  fnfvimad  39773  fvelima2  39789  climrescn  40298  icccncfext  40418  stoweidlem29  40564  stoweidlem59  40594  ovolval4lem1  41184  fnresfnco  41527  funcoressn  41528  fnbrafvb  41555  tz6.12-afv  41574  afvco2  41577  plusfreseq  42097  dfrngc2  42297  dfringc2  42343  rngcresringcat  42355  mndpsuppss  42477  mndpfsupp  42482
  Copyright terms: Public domain W3C validator