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 5242 | . 2 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴) | |
2 | fndm 5192 | . 2 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴) | |
3 | 1, 2 | syl 14 | 1 ⊢ (𝐹:𝐴⟶𝐵 → dom 𝐹 = 𝐴) |
Colors of variables: wff set class |
Syntax hints: → wi 4 = wceq 1316 dom cdm 4509 Fn wfn 5088 ⟶wf 5089 |
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 5096 df-f 5097 |
This theorem is referenced by: fdmd 5249 fdmi 5250 fssxp 5260 ffdm 5263 dmfex 5282 f00 5284 f0dom0 5286 f0rn0 5287 foima 5320 foco 5325 resdif 5357 fimacnv 5517 dff3im 5533 ffvresb 5551 resflem 5552 fmptco 5554 fornex 5981 issmo2 6154 smoiso 6167 tfrcllemubacc 6224 rdgon 6251 frecabcl 6264 frecsuclem 6271 mapprc 6514 elpm2r 6528 map0b 6549 mapsn 6552 brdomg 6610 fopwdom 6698 casef 6941 nn0supp 8997 frecuzrdgdomlem 10158 frecuzrdgsuctlem 10164 zfz1isolemiso 10550 ennnfonelemex 11854 iscnp3 12299 cnpnei 12315 cnntr 12321 cncnp 12326 cndis 12337 psmetdmdm 12420 xmetres 12478 metres 12479 metcnp 12608 dvcj 12769 nninfall 13131 |
Copyright terms: Public domain | W3C validator |