Theorem fndm 5315

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

Syntax hints:   → wi 4   = wceq 1353  dom cdm 4626  Fun wfun 5210   Fn wfn 5211

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 5219

This theorem is referenced by:  funfni  5316  fndmu  5317  fnbr  5318  fnco  5324  fnresdm  5325  fnresdisj  5326  fnssresb  5328  fn0  5335  fnimadisj  5336  fnimaeq0  5337  dmmpti  5345  fdm  5371  f1dm  5426  f1odm  5465  f1o00  5496  fvelimab  5572  fvun1  5582  eqfnfv2  5614  fndmdif  5621  fneqeql2  5625  elpreima  5635  fsn2  5690  fconst3m  5735  fconst4m  5736  fnfvima  5751  funiunfvdm  5763  fnunirn  5767  dff13  5768  f1eqcocnv  5791  oprssov  6015  offval  6089  ofrfval  6090  fnexALT  6111  dmmpo  6205  dmmpoga  6208  tposfo2  6267  smodm2  6295  smoel2  6303  tfrlem5  6314  tfrlem8  6318  tfrlem9  6319  tfrlemisucaccv  6325  tfrlemiubacc  6330  tfrexlem  6334  tfri2d  6336  tfr1onlemsucaccv  6341  tfr1onlemubacc  6346  tfrcllemsucaccv  6354  tfri2  6366  rdgivallem  6381  ixpprc  6718  ixpssmap2g  6726  ixpssmapg  6727  bren  6746  fndmeng  6809  caseinl  7089  caseinr  7090  cc2lem  7264  dmaddpi  7323  dmmulpi  7324  hashinfom  10757  shftfn  10832  phimullem  12224  ennnfonelemhom  12415  qnnen  12431  fnpr2ob  12758  cldrcl  13572  neiss2  13612  txdis1cn  13748