NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  fndm Unicode version

Theorem fndm 5182
Description: The domain of a function. (Contributed by set.mm contributors, 2-Aug-1994.)
Assertion
Ref Expression
fndm

Proof of Theorem fndm
StepHypRef Expression
1 df-fn 4790 . 2
21simprbi 450 1
Colors of variables: wff setvar class
Syntax hints:   wi 4   wceq 1642   cdm 4772   wfun 4775   wfn 4776
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360  df-fn 4790
This theorem is referenced by:  funfni  5183  fndmu  5184  fnbr  5185  fnco  5191  fnresdm  5192  fnresdisj  5193  fnssresb  5195  fn0  5202  fnimadisj  5203  dmopab2  5209  fdm  5226  f1dm  5261  f1odm  5290  f1o00  5317  fvelimab  5370  fniniseg  5371  fvun1  5379  eqfnfv  5392  eqfnfv2  5393  elpreima  5407  fnasrn  5417  fsn2  5434  fconst3  5457  fconst4  5458  dff13  5471  oprssov  5603  dmmpti  5691  dmmpt2  5734  brfns  5833  dmcross  5847  enmap2lem3  6065  enmap1lem3  6071  enprmaplem3  6078  enprmaplem5  6080  enprmaplem6  6081  nchoicelem18  6306
  Copyright terms: Public domain W3C validator