![]() |
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 5381 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | fndm 5331 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | syl 14 |
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 5235 df-f 5236 |
This theorem is referenced by: fdmd 5388 fdmi 5389 fssxp 5399 ffdm 5402 dmfex 5421 f00 5423 f0dom0 5425 f0rn0 5426 foima 5459 foco 5464 resdif 5499 fimacnv 5662 dff3im 5678 ffvresb 5696 resflem 5697 fmptco 5699 focdmex 6135 issmo2 6309 smoiso 6322 tfrcllemubacc 6379 rdgon 6406 frecabcl 6419 frecsuclem 6426 mapprc 6673 elpm2r 6687 map0b 6708 mapsn 6711 brdomg 6769 pw2f1odclem 6857 fopwdom 6859 casef 7112 nn0supp 9253 frecuzrdgdomlem 10443 frecuzrdgsuctlem 10449 zfz1isolemiso 10846 ennnfonelemex 12460 intopsn 12836 iscnp3 14140 cnpnei 14156 cnntr 14162 cncnp 14167 cndis 14178 psmetdmdm 14261 xmetres 14319 metres 14320 metcnp 14449 dvcj 14610 nninfall 15196 |
Copyright terms: Public domain | W3C validator |