Theorem fndm 5460

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

Syntax hints:   → wi 4   = wceq 1398  dom cdm 4754  Fun wfun 5351   Fn wfn 5352

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 5360

This theorem is referenced by:  fndmi  5461  fndmd  5462  funfni  5463  fndmu  5464  fnbr  5465  fnco  5471  fnresdm  5472  fnresdisj  5473  fnssresb  5475  fn0  5483  fnimadisj  5484  fnimaeq0  5485  dmmpti  5493  fdm  5519  f1dm  5583  f1odm  5623  f1o00  5656  fvelimab  5738  fvun1  5748  eqfnfv2  5781  fndmdif  5788  fneqeql2  5792  elpreima  5802  fsn2  5856  fncofn  5867  fconst3m  5908  fconst4m  5909  fnfvima  5926  funiunfvdm  5942  fnunirn  5946  dff13  5947  f1eqcocnv  5970  oprssov  6204  offval  6283  ofrfval  6284  fnexALT  6313  dmmpo  6413  dmmpoga  6417  suppvalfng  6453  suppvalfn  6454  suppfnss  6470  tposfo2  6511  smodm2  6539  smoel2  6547  tfrlem5  6558  tfrlem8  6562  tfrlem9  6563  tfrlemisucaccv  6569  tfrlemiubacc  6574  tfrexlem  6578  tfri2d  6580  tfr1onlemsucaccv  6585  tfr1onlemubacc  6590  tfrcllemsucaccv  6598  tfri2  6610  rdgivallem  6625  ixpprc  6967  ixpssmap2g  6975  ixpssmapg  6976  bren  6996  fndmeng  7064  caseinl  7395  caseinr  7396  cc2lem  7596  dmaddpi  7656  dmmulpi  7657  hashinfom  11166  shftfn  11534  phimullem  12947  ennnfonelemhom  13250  qnnen  13266  fnpr2ob  13604  cldrcl  15093  neiss2  15133  txdis1cn  15269  uhgrm  16199  upgrfnen  16219  upgrex  16224  umgrfnen  16229