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

Theorem fnfun 6600
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 6497 . 2 (𝐹 Fn 𝐴 ↔ (Fun 𝐹 ∧ dom 𝐹 = 𝐴))
21simplbi 499 1 (𝐹 Fn 𝐴 → Fun 𝐹)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1542  dom cdm 5632  Fun wfun 6488   Fn wfn 6489
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 206  df-an 398  df-fn 6497
This theorem is referenced by:  fnfund  6601  fnrel  6602  funfni  6606  fncofn  6615  fnco  6616  fncoOLD  6617  fnssresb  6621  ffun  6669  f1fun  6738  f1ofun  6784  fnbrfvb  6893  fvelimad  6907  fvelimab  6912  fvun1  6930  elpreima  7006  respreima  7014  rescnvimafod  7022  fnsnr  7108  fnprb  7155  fntpb  7156  fconst3  7160  fnfvima  7180  fnunirn  7198  nvof1o  7223  f1eqcocnv  7244  f1eqcocnvOLD  7245  offun  7624  fnexALT  7876  curry1  8029  curry2  8032  fimaproj  8060  suppvalfng  8092  suppvalfn  8093  suppfnss  8113  fnsuppres  8115  frrlem2  8211  frrlem12  8221  wfrlem2OLD  8248  wfrlem14OLD  8261  tfrlem4  8318  tfrlem5  8319  tfrlem11  8327  tz7.48-2  8381  tz7.49  8384  fndmeng  8938  fnfi  9084  fodomfi  9228  resfnfinfin  9235  fczfsuppd  9282  marypha2lem4  9333  inf0  9516  r1elss  9701  dfac8alem  9924  alephfp  10003  dfac3  10016  dfac9  10031  dfac12lem1  10038  dfac12lem2  10039  r1om  10139  cfsmolem  10165  alephsing  10171  zorn2lem1  10391  zorn2lem5  10395  zorn2lem6  10396  zorn2lem7  10397  ttukeylem3  10406  ttukeylem6  10409  fnct  10432  smobeth  10481  fpwwe2lem8  10533  wunr1om  10614  tskr1om  10662  tskr1om2  10663  uzrdg0i  13819  uzrdgsuci  13820  seqexw  13877  hashkf  14186  cshimadifsn  14676  cshimadifsn0  14677  shftfn  14918  phimullem  16611  imasaddvallem  17371  imasvscaval  17380  lidlval  20614  rspval  20615  psgnghm  20937  iscldtop  22398  2ndcomap  22761  qtoptop  23003  basqtop  23014  qtoprest  23020  kqfvima  23033  isr0  23040  kqreglem1  23044  kqnrmlem1  23046  kqnrmlem2  23047  ustbas  23531  uniiccdif  24894  noextendseq  26967  madeval  27134  oldval  27136  fcoinver  31353  fnpreimac  31415  mdetpmtr1  32208  sseqf  32796  sseqfv2  32798  elorrvc  32867  bnj1371  33445  bnj1497  33476  fnrelpredd  33497  naddcllem  34226  naddov2  34229  naddunif  34241  naddasslem1  34242  naddasslem2  34243  addsval  34271  negsval  34313  negsproplem2  34316  filnetlem4  34785  heibor1lem  36200  diaf11N  39444  dibf11N  39556  dibclN  39557  dihintcl  39739  fnsnbt  40587  ismrc  40927  dnnumch1  41274  aomclem4  41287  aomclem6  41289  fnimafnex  41617  ntrclsfv1  42232  ntrneifv1  42256  finnzfsuppd  42387  fvelima2  43387  climrescn  43884  icccncfext  44023  stoweidlem29  44165  stoweidlem59  44195  ovolval4lem1  44785  fnresfnco  45170  funcoressn  45171  fnfocofob  45206  fnbrafvb  45281  tz6.12-afv  45300  afvco2  45303  tz6.12-afv2  45367  fnbrafv2b  45375  imaelsetpreimafv  45482  imasetpreimafvbijlemfv  45489  imasetpreimafvbijlemfo  45492  plusfreseq  45961  dfrngc2  46165  dfringc2  46211  rngcresringcat  46223  ackvalsuc0val  46668
  Copyright terms: Public domain W3C validator