Theorem f1dm 6743

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

Syntax hints:   → wi 4   = wceq 1540  dom cdm 5631  –1-1→wf1 6497

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 6503  df-f 6504  df-f1 6505

This theorem is referenced by:  f1iun  7903  fnwelem  8088  tposf12  8208  fodomr  9070  domssex  9080  fodomfir  9256  f1dmvrnfibi  9269  f1vrnfibi  9270  acndom  9983  acndom2  9986  ackbij1b  10170  fin1a2lem6  10337  hashf1dmrn  14387  cnt0  23268  cnt1  23272  cnhaus  23276  hmeoimaf1o  23692  uspgr1e  29226  s2f1  32918  lindflbs  33345  rankeq1o  36154  hfninf  36169  eldioph2lem2  42744