Theorem fndm 5367

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 5271	. 2 ⊢ (𝐹 Fn 𝐴 ↔ (Fun 𝐹 ∧ dom 𝐹 = 𝐴))
2	1	simprbi 275	1 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)

Syntax hints:   → wi 4   = wceq 1372  dom cdm 4673  Fun wfun 5262   Fn wfn 5263

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 5271

This theorem is referenced by:  fndmi  5368  fndmd  5369  funfni  5370  fndmu  5371  fnbr  5372  fnco  5378  fnresdm  5379  fnresdisj  5380  fnssresb  5382  fn0  5389  fnimadisj  5390  fnimaeq0  5391  dmmpti  5399  fdm  5425  f1dm  5480  f1odm  5520  f1o00  5551  fvelimab  5629  fvun1  5639  eqfnfv2  5672  fndmdif  5679  fneqeql2  5683  elpreima  5693  fsn2  5748  fconst3m  5793  fconst4m  5794  fnfvima  5809  funiunfvdm  5822  fnunirn  5826  dff13  5827  f1eqcocnv  5850  oprssov  6078  offval  6156  ofrfval  6157  fnexALT  6186  dmmpo  6280  dmmpoga  6284  tposfo2  6343  smodm2  6371  smoel2  6379  tfrlem5  6390  tfrlem8  6394  tfrlem9  6395  tfrlemisucaccv  6401  tfrlemiubacc  6406  tfrexlem  6410  tfri2d  6412  tfr1onlemsucaccv  6417  tfr1onlemubacc  6422  tfrcllemsucaccv  6430  tfri2  6442  rdgivallem  6457  ixpprc  6796  ixpssmap2g  6804  ixpssmapg  6805  bren  6824  fndmeng  6887  caseinl  7175  caseinr  7176  cc2lem  7360  dmaddpi  7420  dmmulpi  7421  hashinfom  10904  shftfn  11054  phimullem  12466  ennnfonelemhom  12705  qnnen  12721  fnpr2ob  13090  cldrcl  14492  neiss2  14532  txdis1cn  14668