Theorem f1dm 6674

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

Syntax hints:   → wi 4   = wceq 1539  dom cdm 5589  –1-1→wf1 6430

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 206  df-an 397  df-fn 6436  df-f 6437  df-f1 6438

This theorem is referenced by:  f1iun  7786  fnwelem  7972  tposf12  8067  fodomr  8915  domssex  8925  f1dmvrnfibi  9103  f1vrnfibi  9104  acndom  9807  acndom2  9810  ackbij1b  9995  fin1a2lem6  10161  cnt0  22497  cnt1  22501  cnhaus  22505  hmeoimaf1o  22921  uspgr1e  27611  s2f1  31219  lindflbs  31574  hashf1dmrn  33075  rankeq1o  34473  hfninf  34488  eldioph2lem2  40583