Theorem fndm 5475

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

Assertion

Ref	Expression
fndm	⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)

Proof of Theorem fndm

Step	Hyp	Ref	Expression
1		df-fn 5375	. 2 ⊢ (𝐹 Fn 𝐴 ↔ (Fun 𝐹 ∧ dom 𝐹 = 𝐴))
2	1	simprbi 275	1 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)

Syntax hints:   → wi 4   = wceq 1402  dom cdm 4769  Fun wfun 5366   Fn wfn 5367

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 5375

This theorem is referenced by:  fndmi  5476  fndmd  5477  funfni  5478  fndmu  5479  fnbr  5480  fnco  5486  fnresdm  5487  fnresdisj  5488  fnssresb  5490  fn0  5498  fnimadisj  5499  fnimaeq0  5500  dmmpti  5508  fdm  5534  f1dm  5598  f1odm  5638  f1o00  5671  fvelimab  5753  fvun1  5763  eqfnfv2  5798  fndmdif  5805  fneqeql2  5809  elpreima  5819  fsn2  5873  fncofn  5884  fconst3m  5925  fconst4m  5926  fnfvima  5943  funiunfvdm  5959  fnunirn  5963  dff13  5964  f1eqcocnv  5987  oprssov  6221  offval  6300  ofrfval  6301  fnexALT  6330  dmmpo  6430  dmmpoga  6434  suppvalfng  6470  suppvalfn  6471  suppfnss  6487  tposfo2  6528  smodm2  6556  smoel2  6564  tfrlem5  6575  tfrlem8  6579  tfrlem9  6580  tfrlemisucaccv  6586  tfrlemiubacc  6591  tfrexlem  6595  tfri2d  6597  tfr1onlemsucaccv  6602  tfr1onlemubacc  6607  tfrcllemsucaccv  6615  tfri2  6627  rdgivallem  6642  ixpprc  6991  ixpssmap2g  6999  ixpssmapg  7000  bren  7020  fndmeng  7088  caseinl  7421  caseinr  7422  cc2lem  7622  dmaddpi  7682  dmmulpi  7683  hashinfom  11195  shftfn  11567  phimullem  12981  ennnfonelemhom  13284  qnnen  13300  fnpr2ob  13638  cldrcl  15126  neiss2  15166  txdis1cn  15302  uhgrm  16233  upgrfnen  16253  upgrex  16258  umgrfnen  16263