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 6569 | . 2 ⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹 Fn 𝐴) | |
2 | fndm 6448 | . 2 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴) | |
3 | 1, 2 | syl 17 | 1 ⊢ (𝐹:𝐴–1-1→𝐵 → dom 𝐹 = 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1528 dom cdm 5548 Fn wfn 6343 –1-1→wf1 6345 |
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 208 df-an 397 df-fn 6351 df-f 6352 df-f1 6353 |
This theorem is referenced by: f1iun 7634 fnwelem 7814 tposf12 7906 fodomr 8656 domssex 8666 f1dmvrnfibi 8796 f1vrnfibi 8797 acndom 9465 acndom2 9468 ackbij1b 9649 fin1a2lem6 9815 cnt0 21882 cnt1 21886 cnhaus 21890 hmeoimaf1o 22306 uspgr1e 26953 s2f1 30548 lindflbs 30867 hashf1dmrn 32252 rankeq1o 33529 hfninf 33544 eldioph2lem2 39236 |
Copyright terms: Public domain | W3C validator |