ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  fndm Structured version   GIF version

Theorem fndm 4924
Description: The domain of a function. (Contributed by NM, 2-Aug-1994.)
Assertion
Ref Expression
fndm (𝐹 Fn A → dom 𝐹 = A)

Proof of Theorem fndm
StepHypRef Expression
1 df-fn 4832 . 2 (𝐹 Fn A ↔ (Fun 𝐹 dom 𝐹 = A))
21simprbi 260 1 (𝐹 Fn A → dom 𝐹 = A)
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1228  dom cdm 4272  Fun wfun 4823   Fn wfn 4824
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100
This theorem depends on definitions:  df-bi 110  df-fn 4832
This theorem is referenced by:  funfni  4925  fndmu  4926  fnbr  4927  fnco  4933  fnresdm  4934  fnresdisj  4935  fnssresb  4937  fn0  4944  fnimadisj  4945  fnimaeq0  4946  dmmpti  4954  fdm  4976  f1dm  5021  f1odm  5055  f1o00  5086  fvelimab  5154  fvun1  5164  eqfnfv2  5191  fndmdif  5197  fneqeql2  5201  elpreima  5211  fsn2  5262  fconst3m  5305  fconst4m  5306  fnfvima  5318  funiunfvdm  5327  fnunirn  5331  dff13  5332  f1eqcocnv  5356  oprssov  5565  offval  5642  ofrfval  5643  fnexALT  5663  dmmpt2  5754  tposfo2  5804  smodm2  5832  smoel2  5840  tfrlem5  5852  tfrlem8  5856  tfrlem9  5857  tfrlemisucaccv  5860  tfrlemiubacc  5865  tfrexlem  5870  tfri2d  5872  tfri2  5874  rdgivallem  5888  frecsuclemdm  5904  dmaddpi  6185  dmmulpi  6186
  Copyright terms: Public domain W3C validator