Theorem f1dm 6553

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

Syntax hints:   → wi 4   = wceq 1538  dom cdm 5519  –1-1→wf1 6321

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 210  df-an 400  df-fn 6327  df-f 6328  df-f1 6329

This theorem is referenced by:  f1iun  7627  fnwelem  7808  tposf12  7900  fodomr  8652  domssex  8662  f1dmvrnfibi  8792  f1vrnfibi  8793  acndom  9462  acndom2  9465  ackbij1b  9650  fin1a2lem6  9816  cnt0  21951  cnt1  21955  cnhaus  21959  hmeoimaf1o  22375  uspgr1e  27034  s2f1  30647  lindflbs  30994  hashf1dmrn  32465  rankeq1o  33745  hfninf  33760  eldioph2lem2  39702