Theorem f1dm 6809

Description: The domain of a one-to-one mapping. (Contributed by NM, 8-Mar-2014.) (Proof shortened by Wolf Lammen, 29-May-2024.)

Assertion

Ref	Expression
f1dm	⊢ (𝐹:𝐴–1-1→𝐵 → dom 𝐹 = 𝐴)

Proof of Theorem f1dm

Step	Hyp	Ref	Expression
1		f1fn 6806	. 2 ⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹 Fn 𝐴)
2	1	fndmd 6674	1 ⊢ (𝐹:𝐴–1-1→𝐵 → dom 𝐹 = 𝐴)

Syntax hints:   → wi 4   = wceq 1537  dom cdm 5689  –1-1→wf1 6560

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 6566  df-f 6567  df-f1 6568

This theorem is referenced by:  f1iun  7967  fnwelem  8155  tposf12  8275  fodomr  9167  domssex  9177  fodomfir  9366  f1dmvrnfibi  9379  f1vrnfibi  9380  acndom  10089  acndom2  10092  ackbij1b  10276  fin1a2lem6  10443  hashf1dmrn  14479  cnt0  23370  cnt1  23374  cnhaus  23378  hmeoimaf1o  23794  uspgr1e  29276  s2f1  32914  lindflbs  33387  rankeq1o  36153  hfninf  36168  eldioph2lem2  42749