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 5126 | . 2 | |
2 | 1 | simprbi 273 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wceq 1331 cdm 4539 wfun 5117 wfn 5118 |
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 5126 |
This theorem is referenced by: funfni 5223 fndmu 5224 fnbr 5225 fnco 5231 fnresdm 5232 fnresdisj 5233 fnssresb 5235 fn0 5242 fnimadisj 5243 fnimaeq0 5244 dmmpti 5252 fdm 5278 f1dm 5333 f1odm 5371 f1o00 5402 fvelimab 5477 fvun1 5487 eqfnfv2 5519 fndmdif 5525 fneqeql2 5529 elpreima 5539 fsn2 5594 fconst3m 5639 fconst4m 5640 fnfvima 5652 funiunfvdm 5664 fnunirn 5668 dff13 5669 f1eqcocnv 5692 oprssov 5912 offval 5989 ofrfval 5990 fnexALT 6011 dmmpo 6103 dmmpoga 6106 tposfo2 6164 smodm2 6192 smoel2 6200 tfrlem5 6211 tfrlem8 6215 tfrlem9 6216 tfrlemisucaccv 6222 tfrlemiubacc 6227 tfrexlem 6231 tfri2d 6233 tfr1onlemsucaccv 6238 tfr1onlemubacc 6243 tfrcllemsucaccv 6251 tfri2 6263 rdgivallem 6278 ixpprc 6613 ixpssmap2g 6621 ixpssmapg 6622 bren 6641 fndmeng 6704 caseinl 6976 caseinr 6977 cc2lem 7081 dmaddpi 7140 dmmulpi 7141 hashinfom 10531 shftfn 10603 phimullem 11908 ennnfonelemhom 11935 qnnen 11951 cldrcl 12281 neiss2 12321 txdis1cn 12457 |
Copyright terms: Public domain | W3C validator |