ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  fndm Structured version   Unicode version

Theorem fndm 4941
Description: The domain of a function. (Contributed by NM, 2-Aug-1994.)
Assertion
Ref Expression
fndm  F  Fn  dom  F

Proof of Theorem fndm
StepHypRef Expression
1 df-fn 4848 . 2  F  Fn  Fun 
F  dom  F
21simprbi 260 1  F  Fn  dom  F
Colors of variables: wff set class
Syntax hints:   wi 4   wceq 1242   dom cdm 4288   Fun wfun 4839    Fn wfn 4840
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100
This theorem depends on definitions:  df-bi 110  df-fn 4848
This theorem is referenced by:  funfni  4942  fndmu  4943  fnbr  4944  fnco  4950  fnresdm  4951  fnresdisj  4952  fnssresb  4954  fn0  4961  fnimadisj  4962  fnimaeq0  4963  dmmpti  4971  fdm  4993  f1dm  5039  f1odm  5073  f1o00  5104  fvelimab  5172  fvun1  5182  eqfnfv2  5209  fndmdif  5215  fneqeql2  5219  elpreima  5229  fsn2  5280  fconst3m  5323  fconst4m  5324  fnfvima  5336  funiunfvdm  5345  fnunirn  5349  dff13  5350  f1eqcocnv  5374  oprssov  5584  offval  5661  ofrfval  5662  fnexALT  5682  dmmpt2  5773  tposfo2  5823  smodm2  5851  smoel2  5859  tfrlem5  5871  tfrlem8  5875  tfrlem9  5876  tfrlemisucaccv  5880  tfrlemiubacc  5885  tfrexlem  5889  tfri2d  5891  tfri2  5893  rdgivallem  5908  frecsuclemdm  5927  bren  6164  fndmeng  6225  dmaddpi  6309  dmmulpi  6310
  Copyright terms: Public domain W3C validator