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

Theorem fndm 5190
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 5094 . 2 (𝐹 Fn 𝐴 ↔ (Fun 𝐹 ∧ dom 𝐹 = 𝐴))
21simprbi 271 1 (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1314  dom cdm 4507  Fun wfun 5085   Fn wfn 5086
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 5094
This theorem is referenced by:  funfni  5191  fndmu  5192  fnbr  5193  fnco  5199  fnresdm  5200  fnresdisj  5201  fnssresb  5203  fn0  5210  fnimadisj  5211  fnimaeq0  5212  dmmpti  5220  fdm  5246  f1dm  5301  f1odm  5337  f1o00  5368  fvelimab  5443  fvun1  5453  eqfnfv2  5485  fndmdif  5491  fneqeql2  5495  elpreima  5505  fsn2  5560  fconst3m  5605  fconst4m  5606  fnfvima  5618  funiunfvdm  5630  fnunirn  5634  dff13  5635  f1eqcocnv  5658  oprssov  5878  offval  5955  ofrfval  5956  fnexALT  5977  dmmpo  6069  dmmpoga  6072  tposfo2  6130  smodm2  6158  smoel2  6166  tfrlem5  6177  tfrlem8  6181  tfrlem9  6182  tfrlemisucaccv  6188  tfrlemiubacc  6193  tfrexlem  6197  tfri2d  6199  tfr1onlemsucaccv  6204  tfr1onlemubacc  6209  tfrcllemsucaccv  6217  tfri2  6229  rdgivallem  6244  ixpprc  6579  ixpssmap2g  6587  ixpssmapg  6588  bren  6607  fndmeng  6670  caseinl  6942  caseinr  6943  dmaddpi  7097  dmmulpi  7098  hashinfom  10475  shftfn  10547  phimullem  11807  ennnfonelemhom  11834  qnnen  11850  cldrcl  12177  neiss2  12217  txdis1cn  12353
  Copyright terms: Public domain W3C validator