Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > fdm | GIF version |
Description: The domain of a mapping. (Contributed by NM, 2-Aug-1994.) |
Ref | Expression |
---|---|
fdm | ⊢ (𝐹:𝐴⟶𝐵 → dom 𝐹 = 𝐴) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ffn 5272 | . 2 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴) | |
2 | fndm 5222 | . 2 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴) | |
3 | 1, 2 | syl 14 | 1 ⊢ (𝐹:𝐴⟶𝐵 → dom 𝐹 = 𝐴) |
Colors of variables: wff set class |
Syntax hints: → wi 4 = wceq 1331 dom cdm 4539 Fn wfn 5118 ⟶wf 5119 |
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 5126 df-f 5127 |
This theorem is referenced by: fdmd 5279 fdmi 5280 fssxp 5290 ffdm 5293 dmfex 5312 f00 5314 f0dom0 5316 f0rn0 5317 foima 5350 foco 5355 resdif 5389 fimacnv 5549 dff3im 5565 ffvresb 5583 resflem 5584 fmptco 5586 fornex 6013 issmo2 6186 smoiso 6199 tfrcllemubacc 6256 rdgon 6283 frecabcl 6296 frecsuclem 6303 mapprc 6546 elpm2r 6560 map0b 6581 mapsn 6584 brdomg 6642 fopwdom 6730 casef 6973 nn0supp 9029 frecuzrdgdomlem 10190 frecuzrdgsuctlem 10196 zfz1isolemiso 10582 ennnfonelemex 11927 iscnp3 12372 cnpnei 12388 cnntr 12394 cncnp 12399 cndis 12410 psmetdmdm 12493 xmetres 12551 metres 12552 metcnp 12681 dvcj 12842 nninfall 13204 |
Copyright terms: Public domain | W3C validator |