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

Theorem fndm 5026
 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 4933 . 2 (𝐹 Fn 𝐴 ↔ (Fun 𝐹 ∧ dom 𝐹 = 𝐴))
21simprbi 264 1 (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
 Colors of variables: wff set class Syntax hints:   → wi 4   = wceq 1259  dom cdm 4373  Fun wfun 4924   Fn wfn 4925 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104 This theorem depends on definitions:  df-bi 114  df-fn 4933 This theorem is referenced by:  funfni  5027  fndmu  5028  fnbr  5029  fnco  5035  fnresdm  5036  fnresdisj  5037  fnssresb  5039  fn0  5046  fnimadisj  5047  fnimaeq0  5048  dmmpti  5056  fdm  5078  f1dm  5124  f1odm  5158  f1o00  5189  fvelimab  5257  fvun1  5267  eqfnfv2  5294  fndmdif  5300  fneqeql2  5304  elpreima  5314  fsn2  5365  fconst3m  5408  fconst4m  5409  fnfvima  5421  funiunfvdm  5430  fnunirn  5434  dff13  5435  f1eqcocnv  5459  oprssov  5670  offval  5747  ofrfval  5748  fnexALT  5768  dmmpt2  5859  tposfo2  5913  smodm2  5941  smoel2  5949  tfrlem5  5961  tfrlem8  5965  tfrlem9  5966  tfrlemisucaccv  5970  tfrlemiubacc  5975  tfrexlem  5979  tfri2d  5981  tfri2  5983  rdgivallem  5999  frecsuclemdm  6019  bren  6259  fndmeng  6320  dmaddpi  6481  dmmulpi  6482  shftfn  9653
 Copyright terms: Public domain W3C validator