Theorem fndm 5392

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 5293	. 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 4693   Fun wfun 5284   Fn wfn 5285

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 5293

This theorem is referenced by:  fndmi  5393  fndmd  5394  funfni  5395  fndmu  5396  fnbr  5397  fnco  5403  fnresdm  5404  fnresdisj  5405  fnssresb  5407  fn0  5415  fnimadisj  5416  fnimaeq0  5417  dmmpti  5425  fdm  5451  f1dm  5508  f1odm  5548  f1o00  5580  fvelimab  5658  fvun1  5668  eqfnfv2  5701  fndmdif  5708  fneqeql2  5712  elpreima  5722  fsn2  5777  fconst3m  5826  fconst4m  5827  fnfvima  5842  funiunfvdm  5855  fnunirn  5859  dff13  5860  f1eqcocnv  5883  oprssov  6111  offval  6189  ofrfval  6190  fnexALT  6219  dmmpo  6313  dmmpoga  6317  tposfo2  6376  smodm2  6404  smoel2  6412  tfrlem5  6423  tfrlem8  6427  tfrlem9  6428  tfrlemisucaccv  6434  tfrlemiubacc  6439  tfrexlem  6443  tfri2d  6445  tfr1onlemsucaccv  6450  tfr1onlemubacc  6455  tfrcllemsucaccv  6463  tfri2  6475  rdgivallem  6490  ixpprc  6829  ixpssmap2g  6837  ixpssmapg  6838  bren  6858  fndmeng  6926  caseinl  7219  caseinr  7220  cc2lem  7413  dmaddpi  7473  dmmulpi  7474  hashinfom  10960  shftfn  11250  phimullem  12662  ennnfonelemhom  12901  qnnen  12917  fnpr2ob  13287  cldrcl  14689  neiss2  14729  txdis1cn  14865  uhgrm  15789  upgrfnen  15809  upgrex  15814  umgrfnen  15819