Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > f1dm | Structured version Visualization version GIF version |
Description: The domain of a one-to-one mapping. (Contributed by NM, 8-Mar-2014.) |
Ref | Expression |
---|---|
f1dm | ⊢ (𝐹:𝐴–1-1→𝐵 → dom 𝐹 = 𝐴) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | f1fn 6015 | . 2 ⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹 Fn 𝐴) | |
2 | fndm 5904 | . 2 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝐹:𝐴–1-1→𝐵 → dom 𝐹 = 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1475 dom cdm 5038 Fn wfn 5799 –1-1→wf1 5801 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
This theorem depends on definitions: df-bi 196 df-an 385 df-fn 5807 df-f 5808 df-f1 5809 |
This theorem is referenced by: fun11iun 7019 fnwelem 7179 tposf12 7264 ctex 7856 fodomr 7996 domssex 8006 f1dmvrnfibi 8133 f1vrnfibi 8134 acndom 8757 acndom2 8760 ackbij1b 8944 fin1a2lem6 9110 cnt0 20960 cnt1 20964 cnhaus 20968 hmeoimaf1o 21383 uslgra1 25901 usgra1 25902 rankeq1o 31448 hfninf 31463 eldioph2lem2 36342 uspgr1e 40470 |
Copyright terms: Public domain | W3C validator |