![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > fdm | Unicode version |
Description: The domain of a mapping. (Contributed by NM, 2-Aug-1994.) |
Ref | Expression |
---|---|
fdm |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ffn 5161 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | fndm 5113 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | syl 14 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 |
This theorem depends on definitions: df-bi 115 df-fn 5018 df-f 5019 |
This theorem is referenced by: fdmd 5167 fdmi 5168 fssxp 5178 ffdm 5181 dmfex 5200 f00 5202 f0dom0 5204 f0rn0 5205 foima 5238 foco 5243 resdif 5275 fimacnv 5428 dff3im 5444 ffvresb 5461 resflem 5462 fmptco 5464 fornex 5886 issmo2 6054 smoiso 6067 tfrcllemubacc 6124 rdgon 6151 frecabcl 6164 frecsuclem 6171 mapprc 6409 elpm2r 6423 map0b 6444 mapsn 6447 brdomg 6465 fopwdom 6552 casef 6779 nn0supp 8725 frecuzrdgdomlem 9824 frecuzrdgsuctlem 9830 zfz1isolemiso 10244 nninfall 11900 |
Copyright terms: Public domain | W3C validator |