Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > fndm | Unicode version |
Description: The domain of a function. (Contributed by NM, 2-Aug-1994.) |
Ref | Expression |
---|---|
fndm |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-fn 5185 | . 2 | |
2 | 1 | simprbi 273 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wceq 1342 cdm 4598 wfun 5176 wfn 5177 |
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 5185 |
This theorem is referenced by: funfni 5282 fndmu 5283 fnbr 5284 fnco 5290 fnresdm 5291 fnresdisj 5292 fnssresb 5294 fn0 5301 fnimadisj 5302 fnimaeq0 5303 dmmpti 5311 fdm 5337 f1dm 5392 f1odm 5430 f1o00 5461 fvelimab 5536 fvun1 5546 eqfnfv2 5578 fndmdif 5584 fneqeql2 5588 elpreima 5598 fsn2 5653 fconst3m 5698 fconst4m 5699 fnfvima 5713 funiunfvdm 5725 fnunirn 5729 dff13 5730 f1eqcocnv 5753 oprssov 5974 offval 6051 ofrfval 6052 fnexALT 6073 dmmpo 6165 dmmpoga 6168 tposfo2 6226 smodm2 6254 smoel2 6262 tfrlem5 6273 tfrlem8 6277 tfrlem9 6278 tfrlemisucaccv 6284 tfrlemiubacc 6289 tfrexlem 6293 tfri2d 6295 tfr1onlemsucaccv 6300 tfr1onlemubacc 6305 tfrcllemsucaccv 6313 tfri2 6325 rdgivallem 6340 ixpprc 6676 ixpssmap2g 6684 ixpssmapg 6685 bren 6704 fndmeng 6767 caseinl 7047 caseinr 7048 cc2lem 7198 dmaddpi 7257 dmmulpi 7258 hashinfom 10680 shftfn 10752 phimullem 12136 ennnfonelemhom 12291 qnnen 12307 cldrcl 12649 neiss2 12689 txdis1cn 12825 |
Copyright terms: Public domain | W3C validator |