![]() |
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 5365 | . 2 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴) | |
2 | fndm 5315 | . 2 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴) | |
3 | 1, 2 | syl 14 | 1 ⊢ (𝐹:𝐴⟶𝐵 → dom 𝐹 = 𝐴) |
Colors of variables: wff set class |
Syntax hints: → wi 4 = wceq 1353 dom cdm 4626 Fn wfn 5211 ⟶wf 5212 |
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 5219 df-f 5220 |
This theorem is referenced by: fdmd 5372 fdmi 5373 fssxp 5383 ffdm 5386 dmfex 5405 f00 5407 f0dom0 5409 f0rn0 5410 foima 5443 foco 5448 resdif 5483 fimacnv 5645 dff3im 5661 ffvresb 5679 resflem 5680 fmptco 5682 focdmex 6115 issmo2 6289 smoiso 6302 tfrcllemubacc 6359 rdgon 6386 frecabcl 6399 frecsuclem 6406 mapprc 6651 elpm2r 6665 map0b 6686 mapsn 6689 brdomg 6747 fopwdom 6835 casef 7086 nn0supp 9226 frecuzrdgdomlem 10414 frecuzrdgsuctlem 10420 zfz1isolemiso 10814 ennnfonelemex 12409 intopsn 12780 iscnp3 13634 cnpnei 13650 cnntr 13656 cncnp 13661 cndis 13672 psmetdmdm 13755 xmetres 13813 metres 13814 metcnp 13943 dvcj 14104 nninfall 14678 |
Copyright terms: Public domain | W3C validator |