Theorem fndm 5373

Description: The domain of a function. (Contributed by NM, 2-Aug-1994.)

Assertion

Ref	Expression
fndm	|- ( F Fn A -> dom F = A )

Proof of Theorem fndm

Step	Hyp	Ref	Expression
1		df-fn 5274	. 2 |- ( F Fn A <-> ( Fun F /\ dom F = A ) )
2	1	simprbi 275	1 |- ( F Fn A -> dom F = A )

Syntax hints:   -> wi 4   = wceq 1373   dom cdm 4675   Fun wfun 5265   Fn wfn 5266

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107

This theorem depends on definitions:  df-bi 117  df-fn 5274

This theorem is referenced by:  fndmi  5374  fndmd  5375  funfni  5376  fndmu  5377  fnbr  5378  fnco  5384  fnresdm  5385  fnresdisj  5386  fnssresb  5388  fn0  5395  fnimadisj  5396  fnimaeq0  5397  dmmpti  5405  fdm  5431  f1dm  5486  f1odm  5526  f1o00  5557  fvelimab  5635  fvun1  5645  eqfnfv2  5678  fndmdif  5685  fneqeql2  5689  elpreima  5699  fsn2  5754  fconst3m  5803  fconst4m  5804  fnfvima  5819  funiunfvdm  5832  fnunirn  5836  dff13  5837  f1eqcocnv  5860  oprssov  6088  offval  6166  ofrfval  6167  fnexALT  6196  dmmpo  6290  dmmpoga  6294  tposfo2  6353  smodm2  6381  smoel2  6389  tfrlem5  6400  tfrlem8  6404  tfrlem9  6405  tfrlemisucaccv  6411  tfrlemiubacc  6416  tfrexlem  6420  tfri2d  6422  tfr1onlemsucaccv  6427  tfr1onlemubacc  6432  tfrcllemsucaccv  6440  tfri2  6452  rdgivallem  6467  ixpprc  6806  ixpssmap2g  6814  ixpssmapg  6815  bren  6835  fndmeng  6902  caseinl  7193  caseinr  7194  cc2lem  7378  dmaddpi  7438  dmmulpi  7439  hashinfom  10923  shftfn  11135  phimullem  12547  ennnfonelemhom  12786  qnnen  12802  fnpr2ob  13172  cldrcl  14574  neiss2  14614  txdis1cn  14750