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

Theorem fnfun 6446
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 6351 . 2 (𝐹 Fn 𝐴 ↔ (Fun 𝐹 ∧ dom 𝐹 = 𝐴))
21simplbi 498 1 (𝐹 Fn 𝐴 → Fun 𝐹)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1528  dom cdm 5548  Fun wfun 6342   Fn wfn 6343
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 208  df-an 397  df-fn 6351
This theorem is referenced by:  fnrel  6447  funfni  6450  fnco  6458  fnssresb  6462  ffun  6510  f1fun  6570  f1ofun  6610  fnbrfvb  6711  fvelimad  6725  fvelimab  6730  fvun1  6747  elpreima  6820  respreima  6828  fnsnr  6919  fnprb  6962  fntpb  6963  fconst3  6967  fnfvima  6986  fnunirn  7003  nvof1o  7028  f1eqcocnv  7048  fnexALT  7641  curry1  7788  curry2  7791  fimaproj  7818  suppvalfn  7826  suppfnss  7844  fnsuppres  7846  wfrlem2  7944  wfrlem14  7957  tfrlem4  8004  tfrlem5  8005  tfrlem11  8013  tz7.48-2  8067  tz7.49  8070  fndmeng  8575  fnfi  8784  fodomfi  8785  resfnfinfin  8792  fczfsuppd  8839  marypha2lem4  8890  inf0  9072  r1elss  9223  dfac8alem  9443  alephfp  9522  dfac3  9535  dfac9  9550  dfac12lem1  9557  dfac12lem2  9558  r1om  9654  cfsmolem  9680  alephsing  9686  zorn2lem1  9906  zorn2lem5  9910  zorn2lem6  9911  zorn2lem7  9912  ttukeylem3  9921  ttukeylem6  9924  fnct  9947  smobeth  9996  fpwwe2lem9  10048  wunr1om  10129  tskr1om  10177  tskr1om2  10178  uzrdg0i  13315  uzrdgsuci  13316  seqexw  13373  hashkf  13680  cshimadifsn  14179  cshimadifsn0  14180  shftfn  14420  phimullem  16104  imasaddvallem  16790  imasvscaval  16799  lcomfsupp  19603  lidlval  19893  rspval  19894  psrbagev1  20218  psgnghm  20652  frlmsslsp  20868  iscldtop  21631  2ndcomap  21994  qtoptop  22236  basqtop  22247  qtoprest  22253  kqfvima  22266  isr0  22273  kqreglem1  22277  kqnrmlem1  22279  kqnrmlem2  22280  elrnust  22760  ustbas  22763  uniiccdif  24106  fcoinver  30285  fnpreimac  30344  mdetpmtr1  30987  sseqf  31549  sseqfv2  31551  elorrvc  31620  bnj930  31940  bnj1371  32198  bnj1497  32229  frrlem2  33021  frrlem12  33031  noextendseq  33071  madeval  33186  filnetlem4  33626  heibor1lem  34968  diaf11N  38065  dibf11N  38177  dibclN  38178  dihintcl  38360  fnsnbt  38998  ismrc  39176  dnnumch1  39522  aomclem4  39535  aomclem6  39537  ntrclsfv1  40283  ntrneifv1  40307  fvelima2  41408  climrescn  41905  icccncfext  42046  stoweidlem29  42191  stoweidlem59  42221  ovolval4lem1  42808  fnresfnco  43153  funcoressn  43154  fnbrafvb  43230  tz6.12-afv  43249  afvco2  43252  tz6.12-afv2  43316  fnbrafv2b  43324  imaelsetpreimafv  43432  imasetpreimafvbijlemfv  43439  imasetpreimafvbijlemfo  43442  plusfreseq  43916  dfrngc2  44171  dfringc2  44217  rngcresringcat  44229  mndpsuppss  44347  mndpfsupp  44352
  Copyright terms: Public domain W3C validator