Theorem fndm 5230

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

Syntax hints:   → wi 4   = wceq 1332  dom cdm 4547  Fun wfun 5125   Fn wfn 5126

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106

This theorem depends on definitions:  df-bi 116  df-fn 5134

This theorem is referenced by:  funfni  5231  fndmu  5232  fnbr  5233  fnco  5239  fnresdm  5240  fnresdisj  5241  fnssresb  5243  fn0  5250  fnimadisj  5251  fnimaeq0  5252  dmmpti  5260  fdm  5286  f1dm  5341  f1odm  5379  f1o00  5410  fvelimab  5485  fvun1  5495  eqfnfv2  5527  fndmdif  5533  fneqeql2  5537  elpreima  5547  fsn2  5602  fconst3m  5647  fconst4m  5648  fnfvima  5660  funiunfvdm  5672  fnunirn  5676  dff13  5677  f1eqcocnv  5700  oprssov  5920  offval  5997  ofrfval  5998  fnexALT  6019  dmmpo  6111  dmmpoga  6114  tposfo2  6172  smodm2  6200  smoel2  6208  tfrlem5  6219  tfrlem8  6223  tfrlem9  6224  tfrlemisucaccv  6230  tfrlemiubacc  6235  tfrexlem  6239  tfri2d  6241  tfr1onlemsucaccv  6246  tfr1onlemubacc  6251  tfrcllemsucaccv  6259  tfri2  6271  rdgivallem  6286  ixpprc  6621  ixpssmap2g  6629  ixpssmapg  6630  bren  6649  fndmeng  6712  caseinl  6984  caseinr  6985  cc2lem  7098  dmaddpi  7157  dmmulpi  7158  hashinfom  10556  shftfn  10628  phimullem  11937  ennnfonelemhom  11964  qnnen  11980  cldrcl  12310  neiss2  12350  txdis1cn  12486