Theorem f1dm 6763

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

Syntax hints:   → wi 4   = wceq 1540  dom cdm 5641  –1-1→wf1 6511

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 6517  df-f 6518  df-f1 6519

This theorem is referenced by:  f1iun  7925  fnwelem  8113  tposf12  8233  fodomr  9098  domssex  9108  fodomfir  9286  f1dmvrnfibi  9299  f1vrnfibi  9300  acndom  10011  acndom2  10014  ackbij1b  10198  fin1a2lem6  10365  hashf1dmrn  14415  cnt0  23240  cnt1  23244  cnhaus  23248  hmeoimaf1o  23664  uspgr1e  29178  s2f1  32873  lindflbs  33357  rankeq1o  36166  hfninf  36181  eldioph2lem2  42756