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

Theorem fndm 5192
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 5096 . 2 (𝐹 Fn 𝐴 ↔ (Fun 𝐹 ∧ dom 𝐹 = 𝐴))
21simprbi 273 1 (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1316  dom cdm 4509  Fun wfun 5087   Fn wfn 5088
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 5096
This theorem is referenced by:  funfni  5193  fndmu  5194  fnbr  5195  fnco  5201  fnresdm  5202  fnresdisj  5203  fnssresb  5205  fn0  5212  fnimadisj  5213  fnimaeq0  5214  dmmpti  5222  fdm  5248  f1dm  5303  f1odm  5339  f1o00  5370  fvelimab  5445  fvun1  5455  eqfnfv2  5487  fndmdif  5493  fneqeql2  5497  elpreima  5507  fsn2  5562  fconst3m  5607  fconst4m  5608  fnfvima  5620  funiunfvdm  5632  fnunirn  5636  dff13  5637  f1eqcocnv  5660  oprssov  5880  offval  5957  ofrfval  5958  fnexALT  5979  dmmpo  6071  dmmpoga  6074  tposfo2  6132  smodm2  6160  smoel2  6168  tfrlem5  6179  tfrlem8  6183  tfrlem9  6184  tfrlemisucaccv  6190  tfrlemiubacc  6195  tfrexlem  6199  tfri2d  6201  tfr1onlemsucaccv  6206  tfr1onlemubacc  6211  tfrcllemsucaccv  6219  tfri2  6231  rdgivallem  6246  ixpprc  6581  ixpssmap2g  6589  ixpssmapg  6590  bren  6609  fndmeng  6672  caseinl  6944  caseinr  6945  dmaddpi  7101  dmmulpi  7102  hashinfom  10492  shftfn  10564  phimullem  11828  ennnfonelemhom  11855  qnnen  11871  cldrcl  12198  neiss2  12238  txdis1cn  12374
  Copyright terms: Public domain W3C validator