Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > fndm | GIF version |
Description: The domain of a function. (Contributed by NM, 2-Aug-1994.) |
Ref | Expression |
---|---|
fndm | ⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-fn 4925 | . 2 ⊢ (𝐹 Fn 𝐴 ↔ (Fun 𝐹 ∧ dom 𝐹 = 𝐴)) | |
2 | 1 | simprbi 269 | 1 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴) |
Colors of variables: wff set class |
Syntax hints: → wi 4 = wceq 1284 dom cdm 4363 Fun wfun 4916 Fn wfn 4917 |
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 4925 |
This theorem is referenced by: funfni 5019 fndmu 5020 fnbr 5021 fnco 5027 fnresdm 5028 fnresdisj 5029 fnssresb 5031 fn0 5038 fnimadisj 5039 fnimaeq0 5040 dmmpti 5048 fdm 5070 f1dm 5116 f1odm 5150 f1o00 5181 fvelimab 5250 fvun1 5260 eqfnfv2 5287 fndmdif 5293 fneqeql2 5297 elpreima 5307 fsn2 5358 fconst3m 5401 fconst4m 5402 fnfvima 5414 funiunfvdm 5423 fnunirn 5427 dff13 5428 f1eqcocnv 5451 oprssov 5662 offval 5739 ofrfval 5740 fnexALT 5760 dmmpt2 5851 tposfo2 5905 smodm2 5933 smoel2 5941 tfrlem5 5953 tfrlem8 5957 tfrlem9 5958 tfrlemisucaccv 5962 tfrlemiubacc 5967 tfrexlem 5971 tfri2d 5973 tfri2 5975 rdgivallem 5991 frecsuclemdm 6011 bren 6251 fndmeng 6312 dmaddpi 6515 dmmulpi 6516 shftfn 9712 |
Copyright terms: Public domain | W3C validator |