Theorem fndm 5183

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 4791	. 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 4773  Fun wfun 4776   Fn wfn 4777

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 177  df-an 360  df-fn 4791

This theorem is referenced by:  funfni  5184  fndmu  5185  fnbr  5186  fnco  5192  fnresdm  5193  fnresdisj  5194  fnssresb  5196  fn0  5203  fnimadisj  5204  dmopab2  5210  fdm  5227  f1dm  5262  f1odm  5291  f1o00  5318  fvelimab  5371  fniniseg  5372  fvun1  5380  eqfnfv  5393  eqfnfv2  5394  elpreima  5408  fnasrn  5418  fsn2  5435  fconst3  5458  fconst4  5459  dff13  5472  oprssov  5604  dmmpti  5692  dmmpt2  5735  brfns  5834  dmcross  5848  enmap2lem3  6066  enmap1lem3  6072  enprmaplem3  6079  enprmaplem5  6081  enprmaplem6  6082  nchoicelem18  6307