|   | 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.) (Proof shortened by Wolf Lammen, 29-May-2024.) | 
| Ref | Expression | 
|---|---|
| f1dm | ⊢ (𝐹:𝐴–1-1→𝐵 → dom 𝐹 = 𝐴) | 
| Step | Hyp | Ref | Expression | 
|---|---|---|---|
| 1 | f1fn 6805 | . 2 ⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹 Fn 𝐴) | |
| 2 | 1 | fndmd 6673 | 1 ⊢ (𝐹:𝐴–1-1→𝐵 → dom 𝐹 = 𝐴) | 
| Colors of variables: wff setvar class | 
| Syntax hints: → wi 4 = wceq 1540 dom cdm 5685 –1-1→wf1 6558 | 
| 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 207 df-an 396 df-fn 6564 df-f 6565 df-f1 6566 | 
| This theorem is referenced by: f1iun 7968 fnwelem 8156 tposf12 8276 fodomr 9168 domssex 9178 fodomfir 9368 f1dmvrnfibi 9381 f1vrnfibi 9382 acndom 10091 acndom2 10094 ackbij1b 10278 fin1a2lem6 10445 hashf1dmrn 14482 cnt0 23354 cnt1 23358 cnhaus 23362 hmeoimaf1o 23778 uspgr1e 29261 s2f1 32929 lindflbs 33407 rankeq1o 36172 hfninf 36187 eldioph2lem2 42772 | 
| Copyright terms: Public domain | W3C validator |