Theorem f1dm 6768

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 6763	. 2 ⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹 Fn 𝐴)
2	1	fndmd 6628	1 ⊢ (𝐹:𝐴–1-1→𝐵 → dom 𝐹 = 𝐴)

Syntax hints:   → wi 4   = wceq 1562  dom cdm 5649  –1-1→wf1 6520

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 209  df-an 400  df-fn 6526  df-f 6527  df-f1 6528

This theorem is referenced by:  f1iun  7927  fnwelem  8113  tposf12  8233  fodomr  9102  domssex  9112  fodomfir  9274  f1dmvrnfibi  9286  f1vrnfibi  9287  acndom  10009  acndom2  10012  ackbij1b  10196  fin1a2lem6  10364  hashf1dmrn  14458  cnt0  23408  cnt1  23412  cnhaus  23416  hmeoimaf1o  23832  uspgr1e  29447  s2f1  33125  lindflbs  33567  fineqvinfep  35425  vonf1wev  35455  rankeq1o  36526  hfninf  36541  eldioph2lem2  43347