Theorem fndm 5297

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 5201	. 2 |- ( F Fn A <-> ( Fun F /\ dom F = A ) )
2	1	simprbi 273	1 |- ( F Fn A -> dom F = A )

Syntax hints:   -> wi 4   = wceq 1348   dom cdm 4611   Fun wfun 5192   Fn wfn 5193

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

This theorem depends on definitions:  df-bi 116  df-fn 5201

This theorem is referenced by:  funfni  5298  fndmu  5299  fnbr  5300  fnco  5306  fnresdm  5307  fnresdisj  5308  fnssresb  5310  fn0  5317  fnimadisj  5318  fnimaeq0  5319  dmmpti  5327  fdm  5353  f1dm  5408  f1odm  5446  f1o00  5477  fvelimab  5552  fvun1  5562  eqfnfv2  5594  fndmdif  5601  fneqeql2  5605  elpreima  5615  fsn2  5670  fconst3m  5715  fconst4m  5716  fnfvima  5730  funiunfvdm  5742  fnunirn  5746  dff13  5747  f1eqcocnv  5770  oprssov  5994  offval  6068  ofrfval  6069  fnexALT  6090  dmmpo  6184  dmmpoga  6187  tposfo2  6246  smodm2  6274  smoel2  6282  tfrlem5  6293  tfrlem8  6297  tfrlem9  6298  tfrlemisucaccv  6304  tfrlemiubacc  6309  tfrexlem  6313  tfri2d  6315  tfr1onlemsucaccv  6320  tfr1onlemubacc  6325  tfrcllemsucaccv  6333  tfri2  6345  rdgivallem  6360  ixpprc  6697  ixpssmap2g  6705  ixpssmapg  6706  bren  6725  fndmeng  6788  caseinl  7068  caseinr  7069  cc2lem  7228  dmaddpi  7287  dmmulpi  7288  hashinfom  10712  shftfn  10788  phimullem  12179  ennnfonelemhom  12370  qnnen  12386  cldrcl  12896  neiss2  12936  txdis1cn  13072