| 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 10679 frecuzrdgsuctlem 10685 zfz1isolemiso 11103 ennnfonelemex 13036 intopsn 13451 iscnp3 14929 cnpnei 14945 cnntr 14951 cncnp 14956 cndis 14967 psmetdmdm 15050 xmetres 15108 metres 15109 metcnp 15238 dvcj 15435 wlkm 16192 upgr2wlkdc 16230 wlkres 16232 nninfall 16614 |
| Copyright terms: Public domain | W3C validator |