Theorem fndm 5420

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

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

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 5321

This theorem is referenced by:  fndmi  5421  fndmd  5422  funfni  5423  fndmu  5424  fnbr  5425  fnco  5431  fnresdm  5432  fnresdisj  5433  fnssresb  5435  fn0  5443  fnimadisj  5444  fnimaeq0  5445  dmmpti  5453  fdm  5479  f1dm  5538  f1odm  5578  f1o00  5610  fvelimab  5692  fvun1  5702  eqfnfv2  5735  fndmdif  5742  fneqeql2  5746  elpreima  5756  fsn2  5811  fncofn  5821  fconst3m  5862  fconst4m  5863  fnfvima  5878  funiunfvdm  5893  fnunirn  5897  dff13  5898  f1eqcocnv  5921  oprssov  6153  offval  6232  ofrfval  6233  fnexALT  6262  dmmpo  6356  dmmpoga  6360  tposfo2  6419  smodm2  6447  smoel2  6455  tfrlem5  6466  tfrlem8  6470  tfrlem9  6471  tfrlemisucaccv  6477  tfrlemiubacc  6482  tfrexlem  6486  tfri2d  6488  tfr1onlemsucaccv  6493  tfr1onlemubacc  6498  tfrcllemsucaccv  6506  tfri2  6518  rdgivallem  6533  ixpprc  6874  ixpssmap2g  6882  ixpssmapg  6883  bren  6903  fndmeng  6971  caseinl  7269  caseinr  7270  cc2lem  7463  dmaddpi  7523  dmmulpi  7524  hashinfom  11012  shftfn  11350  phimullem  12762  ennnfonelemhom  13001  qnnen  13017  fnpr2ob  13388  cldrcl  14791  neiss2  14831  txdis1cn  14967  uhgrm  15893  upgrfnen  15913  upgrex  15918  umgrfnen  15923