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

Theorem fndm 5099
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 5005 . 2 (𝐹 Fn 𝐴 ↔ (Fun 𝐹 ∧ dom 𝐹 = 𝐴))
21simprbi 269 1 (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1289  dom cdm 4428  Fun wfun 4996   Fn wfn 4997
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105
This theorem depends on definitions:  df-bi 115  df-fn 5005
This theorem is referenced by:  funfni  5100  fndmu  5101  fnbr  5102  fnco  5108  fnresdm  5109  fnresdisj  5110  fnssresb  5112  fn0  5119  fnimadisj  5120  fnimaeq0  5121  dmmpti  5129  fdm  5152  f1dm  5205  f1odm  5241  f1o00  5272  fvelimab  5344  fvun1  5354  eqfnfv2  5382  fndmdif  5388  fneqeql2  5392  elpreima  5402  fsn2  5455  fconst3m  5498  fconst4m  5499  fnfvima  5511  funiunfvdm  5524  fnunirn  5528  dff13  5529  f1eqcocnv  5552  oprssov  5768  offval  5845  ofrfval  5846  fnexALT  5866  dmmpt2  5957  tposfo2  6014  smodm2  6042  smoel2  6050  tfrlem5  6061  tfrlem8  6065  tfrlem9  6066  tfrlemisucaccv  6072  tfrlemiubacc  6077  tfrexlem  6081  tfri2d  6083  tfr1onlemsucaccv  6088  tfr1onlemubacc  6093  tfrcllemsucaccv  6101  tfri2  6113  rdgivallem  6128  bren  6444  fndmeng  6507  dmaddpi  6863  dmmulpi  6864  hashinfom  10151  shftfn  10223  phimullem  11283
  Copyright terms: Public domain W3C validator