Theorem fnfun 5694

Description: A function with domain is a function. (Contributed by NM, 1-Aug-1994.)

Assertion

Ref	Expression
fnfun	|- ( F Fn A -> Fun F )

Proof of Theorem fnfun

Step	Hyp	Ref	Expression
1		df-fn 5603	. 2 |- ( F Fn A <-> ( Fun F /\ dom F = A ) )
2	1	simplbi 466	1 |- ( F Fn A -> Fun F )

Syntax hints:   -> wi 4   = wceq 1454   dom cdm 4852   Fun wfun 5594   Fn wfn 5595

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 190  df-an 377  df-fn 5603

This theorem is referenced by:  fnrel  5695  funfni  5697  fnco  5705  fnssresb  5709  ffun  5753  f1fun  5803  f1ofun  5838  fnbrfvb  5927  fvelimab  5943  fvun1  5958  elpreima  6024  respreima  6031  fnsnb  6106  fnprb  6146  fntpb  6147  fconst3  6152  fnfvima  6167  fnunirn  6182  nvof1o  6203  f1eqcocnv  6223  fnexALT  6785  curry1  6914  curry2  6917  suppvalfn  6947  suppfnss  6966  fnsuppres  6968  wfrlem2  7061  wfrlem14  7074  tfrlem4  7122  tfrlem5  7123  tfrlem11  7131  tz7.48-2  7184  tz7.49  7187  fndmeng  7671  fnfi  7874  fodomfi  7875  fczfsuppd  7926  marypha2lem4  7977  inf0  8151  r1elss  8302  dfac8alem  8485  alephfp  8564  dfac3  8577  dfac9  8591  dfac12lem1  8598  dfac12lem2  8599  r1om  8699  cfsmolem  8725  alephsing  8731  zorn2lem1  8951  zorn2lem5  8955  zorn2lem6  8956  zorn2lem7  8957  ttukeylem3  8966  ttukeylem6  8969  smobeth  9036  fpwwe2lem9  9088  wunr1om  9169  tskr1om  9217  tskr1om2  9218  uzrdg0i  12204  uzrdgsuci  12205  hashkf  12548  shftfn  13184  phimullem  14775  imasaddvallem  15483  imasvscaval  15492  frmdss2  16695  lcomfsupp  18176  lidlval  18463  rspval  18464  psrbagev1  18781  psgnghm  19196  frlmsslsp  19402  iscldtop  20159  2ndcomap  20521  qtoptop  20763  basqtop  20774  qtoprest  20780  kqfvima  20793  isr0  20800  kqreglem1  20804  kqnrmlem1  20806  kqnrmlem2  20807  elrnust  21287  ustbas  21290  uniiccdif  22583  eupap1  25752  fcoinver  28262  fnct  28345  mdetpmtr1  28697  fimaproj  28708  sseqf  29273  sseqfv2  29275  elorrvc  29344  bnj142OLD  29582  bnj930  29629  bnj1371  29886  bnj1497  29917  frrlem2  30563  filnetlem4  31085  heibor1lem  32185  diaf11N  34661  dibf11N  34773  dibclN  34774  dihintcl  34956  ismrc  35587  dnnumch1  35946  aomclem4  35959  aomclem6  35961  icccncfext  37802  stoweidlem29  37926  stoweidlem29OLD  37927  stoweidlem59  37957  fnresfnco  38664  funcoressn  38665  fnbrafvb  38693  tz6.12-afv  38712  afvco2  38715  resfnfinfin  39079  plusfreseq  40044  dfrngc2  40246  dfringc2  40292  rngcresringcat  40304  mndpsuppss  40428  mndpfsupp  40433