![]() |
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 5114 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | fndm 5066 |
. 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 4972 df-f 4973 |
This theorem is referenced by: fdmi 5120 fssxp 5127 ffdm 5130 dmfex 5148 f00 5150 f0dom0 5152 f0rn0 5153 foima 5186 foco 5191 resdif 5223 fimacnv 5373 dff3im 5389 ffvresb 5403 resflem 5404 fmptco 5406 fornex 5821 issmo2 5986 smoiso 5999 tfrcllemubacc 6056 rdgon 6083 frecabcl 6096 frecsuclem 6103 mapprc 6339 elpm2r 6353 map0b 6374 mapsn 6377 brdomg 6395 fopwdom 6482 casef 6686 nn0supp 8617 frecuzrdgdomlem 9713 frecuzrdgsuctlem 9719 nninfall 11241 |
Copyright terms: Public domain | W3C validator |