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

Theorem fnfun 5888
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 5793 . 2 (𝐹 Fn 𝐴 ↔ (Fun 𝐹 ∧ dom 𝐹 = 𝐴))
21simplbi 474 1 (𝐹 Fn 𝐴 → Fun 𝐹)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1474  dom cdm 5028  Fun wfun 5784   Fn wfn 5785
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 195  df-an 384  df-fn 5793
This theorem is referenced by:  fnrel  5889  funfni  5891  fnco  5899  fnssresb  5903  ffun  5947  f1fun  6001  f1ofun  6037  fnbrfvb  6131  fvelimab  6148  fvun1  6164  elpreima  6230  respreima  6237  fnsnb  6315  fnprb  6355  fntpb  6356  fconst3  6360  fnfvima  6378  fnunirn  6393  nvof1o  6414  f1eqcocnv  6434  fnexALT  7002  curry1  7133  curry2  7136  suppvalfn  7166  suppfnss  7184  fnsuppres  7186  wfrlem2  7279  wfrlem14  7292  tfrlem4  7339  tfrlem5  7340  tfrlem11  7348  tz7.48-2  7401  tz7.49  7404  fndmeng  7896  fnfi  8100  fodomfi  8101  fczfsuppd  8153  marypha2lem4  8204  inf0  8378  r1elss  8529  dfac8alem  8712  alephfp  8791  dfac3  8804  dfac9  8818  dfac12lem1  8825  dfac12lem2  8826  r1om  8926  cfsmolem  8952  alephsing  8958  zorn2lem1  9178  zorn2lem5  9182  zorn2lem6  9183  zorn2lem7  9184  ttukeylem3  9193  ttukeylem6  9196  smobeth  9264  fpwwe2lem9  9316  wunr1om  9397  tskr1om  9445  tskr1om2  9446  uzrdg0i  12575  uzrdgsuci  12576  hashkf  12936  cshimadifsn  13372  cshimadifsn0  13373  shftfn  13607  phimullem  15268  imasaddvallem  15958  imasvscaval  15967  frmdss2  17169  lcomfsupp  18672  lidlval  18959  rspval  18960  psrbagev1  19277  psgnghm  19690  frlmsslsp  19896  iscldtop  20651  2ndcomap  21013  qtoptop  21255  basqtop  21266  qtoprest  21272  kqfvima  21285  isr0  21292  kqreglem1  21296  kqnrmlem1  21298  kqnrmlem2  21299  elrnust  21780  ustbas  21783  uniiccdif  23069  eupap1  26269  fcoinver  28604  fnct  28682  mdetpmtr1  29023  fimaproj  29034  sseqf  29587  sseqfv2  29589  elorrvc  29658  bnj142OLD  29854  bnj930  29900  bnj1371  30157  bnj1497  30188  frrlem2  30831  filnetlem4  31352  heibor1lem  32574  diaf11N  35152  dibf11N  35264  dibclN  35265  dihintcl  35447  ismrc  36078  dnnumch1  36428  aomclem4  36441  aomclem6  36443  ntrclsfv1  37169  ntrneifv1  37193  icccncfext  38570  stoweidlem29  38719  stoweidlem59  38749  ovolval4lem1  39336  fnresfnco  39652  funcoressn  39653  fnbrafvb  39681  tz6.12-afv  39700  afvco2  39703  resfnfinfin  40159  plusfreseq  41557  dfrngc2  41759  dfringc2  41805  rngcresringcat  41817  mndpsuppss  41941  mndpfsupp  41946
  Copyright terms: Public domain W3C validator