![]() |
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 A → dom 𝐹 = A) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-fn 4848 | . 2 ⊢ (𝐹 Fn A ↔ (Fun 𝐹 ∧ dom 𝐹 = A)) | |
2 | 1 | simprbi 260 | 1 ⊢ (𝐹 Fn A → dom 𝐹 = A) |
Colors of variables: wff set class |
Syntax hints: → wi 4 = wceq 1242 dom cdm 4288 Fun wfun 4839 Fn wfn 4840 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 |
This theorem depends on definitions: df-bi 110 df-fn 4848 |
This theorem is referenced by: funfni 4942 fndmu 4943 fnbr 4944 fnco 4950 fnresdm 4951 fnresdisj 4952 fnssresb 4954 fn0 4961 fnimadisj 4962 fnimaeq0 4963 dmmpti 4971 fdm 4993 f1dm 5039 f1odm 5073 f1o00 5104 fvelimab 5172 fvun1 5182 eqfnfv2 5209 fndmdif 5215 fneqeql2 5219 elpreima 5229 fsn2 5280 fconst3m 5323 fconst4m 5324 fnfvima 5336 funiunfvdm 5345 fnunirn 5349 dff13 5350 f1eqcocnv 5374 oprssov 5584 offval 5661 ofrfval 5662 fnexALT 5682 dmmpt2 5773 tposfo2 5823 smodm2 5851 smoel2 5859 tfrlem5 5871 tfrlem8 5875 tfrlem9 5876 tfrlemisucaccv 5880 tfrlemiubacc 5885 tfrexlem 5889 tfri2d 5891 tfri2 5893 rdgivallem 5908 frecsuclemdm 5927 bren 6164 fndmeng 6225 dmaddpi 6309 dmmulpi 6310 |
Copyright terms: Public domain | W3C validator |