| 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 5271 | . 2 ⊢ (𝐹 Fn 𝐴 ↔ (Fun 𝐹 ∧ dom 𝐹 = 𝐴)) | |
| 2 | 1 | simprbi 275 | 1 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴) |
| Colors of variables: wff set class |
| Syntax hints: → wi 4 = wceq 1372 dom cdm 4673 Fun wfun 5262 Fn wfn 5263 |
| 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 5271 |
| This theorem is referenced by: fndmi 5368 fndmd 5369 funfni 5370 fndmu 5371 fnbr 5372 fnco 5378 fnresdm 5379 fnresdisj 5380 fnssresb 5382 fn0 5389 fnimadisj 5390 fnimaeq0 5391 dmmpti 5399 fdm 5425 f1dm 5480 f1odm 5520 f1o00 5551 fvelimab 5629 fvun1 5639 eqfnfv2 5672 fndmdif 5679 fneqeql2 5683 elpreima 5693 fsn2 5748 fconst3m 5793 fconst4m 5794 fnfvima 5809 funiunfvdm 5822 fnunirn 5826 dff13 5827 f1eqcocnv 5850 oprssov 6078 offval 6156 ofrfval 6157 fnexALT 6186 dmmpo 6280 dmmpoga 6284 tposfo2 6343 smodm2 6371 smoel2 6379 tfrlem5 6390 tfrlem8 6394 tfrlem9 6395 tfrlemisucaccv 6401 tfrlemiubacc 6406 tfrexlem 6410 tfri2d 6412 tfr1onlemsucaccv 6417 tfr1onlemubacc 6422 tfrcllemsucaccv 6430 tfri2 6442 rdgivallem 6457 ixpprc 6796 ixpssmap2g 6804 ixpssmapg 6805 bren 6824 fndmeng 6887 caseinl 7175 caseinr 7176 cc2lem 7360 dmaddpi 7420 dmmulpi 7421 hashinfom 10904 shftfn 11054 phimullem 12466 ennnfonelemhom 12705 qnnen 12721 fnpr2ob 13090 cldrcl 14492 neiss2 14532 txdis1cn 14668 |
| Copyright terms: Public domain | W3C validator |