| 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 5482 | . 2 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴) | |
| 2 | fndm 5429 | . 2 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴) | |
| 3 | 1, 2 | syl 14 | 1 ⊢ (𝐹:𝐴⟶𝐵 → dom 𝐹 = 𝐴) |
| Colors of variables: wff set class |
| Syntax hints: → wi 4 = wceq 1397 dom cdm 4725 Fn wfn 5321 ⟶wf 5322 |
| 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 5329 df-f 5330 |
| This theorem is referenced by: fdmd 5489 fdmi 5490 fssxp 5502 ffdm 5505 dmfex 5526 f00 5528 f0dom0 5530 f0rn0 5531 foima 5564 fimadmfo 5568 foco 5570 resdif 5605 fimacnv 5776 dff3im 5792 ffvresb 5810 resflem 5811 fmptco 5813 focdmex 6277 issmo2 6455 smoiso 6468 tfrcllemubacc 6525 rdgon 6552 frecabcl 6565 frecsuclem 6572 mapprc 6821 elpm2r 6835 map0b 6856 mapsn 6859 brdomg 6919 pw2f1odclem 7020 fopwdom 7022 casef 7287 nn0supp 9454 frecuzrdgdomlem 10680 frecuzrdgsuctlem 10686 zfz1isolemiso 11104 ennnfonelemex 13040 intopsn 13455 iscnp3 14933 cnpnei 14949 cnntr 14955 cncnp 14960 cndis 14971 psmetdmdm 15054 xmetres 15112 metres 15113 metcnp 15242 dvcj 15439 wlkm 16196 upgr2wlkdc 16234 wlkres 16236 nninfall 16637 |
| Copyright terms: Public domain | W3C validator |