Theorem f1dm 6792

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

Syntax hints:   → wi 4   = wceq 1542  dom cdm 5677  –1-1→wf1 6541

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 398  df-fn 6547  df-f 6548  df-f1 6549

This theorem is referenced by:  f1iun  7930  fnwelem  8117  tposf12  8236  fodomr  9128  domssex  9138  f1dmvrnfibi  9336  f1vrnfibi  9337  acndom  10046  acndom2  10049  ackbij1b  10234  fin1a2lem6  10400  hashf1dmrn  14403  cnt0  22850  cnt1  22854  cnhaus  22858  hmeoimaf1o  23274  uspgr1e  28501  s2f1  32111  lindflbs  32495  rankeq1o  35143  hfninf  35158  eldioph2lem2  41499