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

Step	Hyp	Ref	Expression
1		df-fn 4790	. 2 ⊢ (F Fn A ↔ (Fun F ∧ dom F = A))
2	1	simprbi 450	1 ⊢ (F Fn A → dom F = A)

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