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

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

Proof of Theorem fndm
StepHypRef Expression
1 df-fn 4905 . 2 (𝐹 Fn 𝐴 ↔ (Fun 𝐹 ∧ dom 𝐹 = 𝐴))
21simprbi 260 1 (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1243  dom cdm 4345  Fun wfun 4896   Fn wfn 4897
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 4905
This theorem is referenced by:  funfni  4999  fndmu  5000  fnbr  5001  fnco  5007  fnresdm  5008  fnresdisj  5009  fnssresb  5011  fn0  5018  fnimadisj  5019  fnimaeq0  5020  dmmpti  5028  fdm  5050  f1dm  5096  f1odm  5130  f1o00  5161  fvelimab  5229  fvun1  5239  eqfnfv2  5266  fndmdif  5272  fneqeql2  5276  elpreima  5286  fsn2  5337  fconst3m  5380  fconst4m  5381  fnfvima  5393  funiunfvdm  5402  fnunirn  5406  dff13  5407  f1eqcocnv  5431  oprssov  5642  offval  5719  ofrfval  5720  fnexALT  5740  dmmpt2  5831  tposfo2  5882  smodm2  5910  smoel2  5918  tfrlem5  5930  tfrlem8  5934  tfrlem9  5935  tfrlemisucaccv  5939  tfrlemiubacc  5944  tfrexlem  5948  tfri2d  5950  tfri2  5952  rdgivallem  5968  frecsuclemdm  5988  bren  6228  fndmeng  6289  dmaddpi  6423  dmmulpi  6424  shftfn  9425
  Copyright terms: Public domain W3C validator