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

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

Proof of Theorem fndm
StepHypRef Expression
1 df-fn 4790 . 2 (F Fn A ↔ (Fun F dom F = A))
21simprbi 450 1 (F Fn A → dom F = A)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   = wceq 1642  dom cdm 4772  Fun wfun 4775   Fn 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