![]() |
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 5219 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | simprbi 275 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() |
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 5219 |
This theorem is referenced by: funfni 5316 fndmu 5317 fnbr 5318 fnco 5324 fnresdm 5325 fnresdisj 5326 fnssresb 5328 fn0 5335 fnimadisj 5336 fnimaeq0 5337 dmmpti 5345 fdm 5371 f1dm 5426 f1odm 5465 f1o00 5496 fvelimab 5572 fvun1 5582 eqfnfv2 5614 fndmdif 5621 fneqeql2 5625 elpreima 5635 fsn2 5690 fconst3m 5735 fconst4m 5736 fnfvima 5751 funiunfvdm 5763 fnunirn 5767 dff13 5768 f1eqcocnv 5791 oprssov 6015 offval 6089 ofrfval 6090 fnexALT 6111 dmmpo 6205 dmmpoga 6208 tposfo2 6267 smodm2 6295 smoel2 6303 tfrlem5 6314 tfrlem8 6318 tfrlem9 6319 tfrlemisucaccv 6325 tfrlemiubacc 6330 tfrexlem 6334 tfri2d 6336 tfr1onlemsucaccv 6341 tfr1onlemubacc 6346 tfrcllemsucaccv 6354 tfri2 6366 rdgivallem 6381 ixpprc 6718 ixpssmap2g 6726 ixpssmapg 6727 bren 6746 fndmeng 6809 caseinl 7089 caseinr 7090 cc2lem 7264 dmaddpi 7323 dmmulpi 7324 hashinfom 10753 shftfn 10828 phimullem 12219 ennnfonelemhom 12410 qnnen 12426 cldrcl 13495 neiss2 13535 txdis1cn 13671 |
Copyright terms: Public domain | W3C validator |