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 5331 | . 2 | |
2 | fndm 5281 | . 2 | |
3 | 1, 2 | syl 14 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wceq 1342 cdm 4598 wfn 5177 wf 5178 |
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 df-f 5186 |
This theorem is referenced by: fdmd 5338 fdmi 5339 fssxp 5349 ffdm 5352 dmfex 5371 f00 5373 f0dom0 5375 f0rn0 5376 foima 5409 foco 5414 resdif 5448 fimacnv 5608 dff3im 5624 ffvresb 5642 resflem 5643 fmptco 5645 fornex 6075 issmo2 6248 smoiso 6261 tfrcllemubacc 6318 rdgon 6345 frecabcl 6358 frecsuclem 6365 mapprc 6609 elpm2r 6623 map0b 6644 mapsn 6647 brdomg 6705 fopwdom 6793 casef 7044 nn0supp 9157 frecuzrdgdomlem 10342 frecuzrdgsuctlem 10348 zfz1isolemiso 10738 ennnfonelemex 12290 iscnp3 12750 cnpnei 12766 cnntr 12772 cncnp 12777 cndis 12788 psmetdmdm 12871 xmetres 12929 metres 12930 metcnp 13059 dvcj 13220 nninfall 13730 |
Copyright terms: Public domain | W3C validator |