Theorem f1dm 6658

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

Syntax hints:   → wi 4   = wceq 1539  dom cdm 5580  –1-1→wf1 6415

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 396  df-fn 6421  df-f 6422  df-f1 6423

This theorem is referenced by:  f1iun  7760  fnwelem  7943  tposf12  8038  fodomr  8864  domssex  8874  f1dmvrnfibi  9033  f1vrnfibi  9034  acndom  9738  acndom2  9741  ackbij1b  9926  fin1a2lem6  10092  cnt0  22405  cnt1  22409  cnhaus  22413  hmeoimaf1o  22829  uspgr1e  27514  s2f1  31121  lindflbs  31476  hashf1dmrn  32975  rankeq1o  34400  hfninf  34415  eldioph2lem2  40499