Theorem fndm 5419

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

Syntax hints:   → wi 4   = wceq 1395  dom cdm 4718  Fun wfun 5311   Fn wfn 5312

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 5320

This theorem is referenced by:  fndmi  5420  fndmd  5421  funfni  5422  fndmu  5423  fnbr  5424  fnco  5430  fnresdm  5431  fnresdisj  5432  fnssresb  5434  fn0  5442  fnimadisj  5443  fnimaeq0  5444  dmmpti  5452  fdm  5478  f1dm  5535  f1odm  5575  f1o00  5607  fvelimab  5689  fvun1  5699  eqfnfv2  5732  fndmdif  5739  fneqeql2  5743  elpreima  5753  fsn2  5808  fconst3m  5857  fconst4m  5858  fnfvima  5873  funiunfvdm  5886  fnunirn  5890  dff13  5891  f1eqcocnv  5914  oprssov  6146  offval  6224  ofrfval  6225  fnexALT  6254  dmmpo  6348  dmmpoga  6352  tposfo2  6411  smodm2  6439  smoel2  6447  tfrlem5  6458  tfrlem8  6462  tfrlem9  6463  tfrlemisucaccv  6469  tfrlemiubacc  6474  tfrexlem  6478  tfri2d  6480  tfr1onlemsucaccv  6485  tfr1onlemubacc  6490  tfrcllemsucaccv  6498  tfri2  6510  rdgivallem  6525  ixpprc  6864  ixpssmap2g  6872  ixpssmapg  6873  bren  6893  fndmeng  6961  caseinl  7254  caseinr  7255  cc2lem  7448  dmaddpi  7508  dmmulpi  7509  hashinfom  10995  shftfn  11330  phimullem  12742  ennnfonelemhom  12981  qnnen  12997  fnpr2ob  13368  cldrcl  14770  neiss2  14810  txdis1cn  14946  uhgrm  15872  upgrfnen  15892  upgrex  15897  umgrfnen  15902