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

Theorem fndm 5315
Description: The domain of a function. (Contributed by NM, 2-Aug-1994.)
Assertion
Ref Expression
fndm  |-  ( F  Fn  A  ->  dom  F  =  A )

Proof of Theorem fndm
StepHypRef Expression
1 df-fn 5219 . 2  |-  ( F  Fn  A  <->  ( Fun  F  /\  dom  F  =  A ) )
21simprbi 275 1  |-  ( F  Fn  A  ->  dom  F  =  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1353   dom cdm 4626   Fun wfun 5210    Fn wfn 5211
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107
This theorem depends on definitions:  df-bi 117  df-fn 5219
This theorem is referenced by:  funfni  5316  fndmu  5317  fnbr  5318  fnco  5324  fnresdm  5325  fnresdisj  5326  fnssresb  5328  fn0  5335  fnimadisj  5336  fnimaeq0  5337  dmmpti  5345  fdm  5371  f1dm  5426  f1odm  5465  f1o00  5496  fvelimab  5572  fvun1  5582  eqfnfv2  5614  fndmdif  5621  fneqeql2  5625  elpreima  5635  fsn2  5690  fconst3m  5735  fconst4m  5736  fnfvima  5751  funiunfvdm  5763  fnunirn  5767  dff13  5768  f1eqcocnv  5791  oprssov  6015  offval  6089  ofrfval  6090  fnexALT  6111  dmmpo  6205  dmmpoga  6208  tposfo2  6267  smodm2  6295  smoel2  6303  tfrlem5  6314  tfrlem8  6318  tfrlem9  6319  tfrlemisucaccv  6325  tfrlemiubacc  6330  tfrexlem  6334  tfri2d  6336  tfr1onlemsucaccv  6341  tfr1onlemubacc  6346  tfrcllemsucaccv  6354  tfri2  6366  rdgivallem  6381  ixpprc  6718  ixpssmap2g  6726  ixpssmapg  6727  bren  6746  fndmeng  6809  caseinl  7089  caseinr  7090  cc2lem  7264  dmaddpi  7323  dmmulpi  7324  hashinfom  10757  shftfn  10832  phimullem  12224  ennnfonelemhom  12415  qnnen  12431  fnpr2ob  12758  cldrcl  13572  neiss2  13612  txdis1cn  13748
  Copyright terms: Public domain W3C validator