Theorem f1dm 6760

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

Syntax hints:   → wi 4   = wceq 1540  dom cdm 5638  –1-1→wf1 6508

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 6514  df-f 6515  df-f1 6516

This theorem is referenced by:  f1iun  7922  fnwelem  8110  tposf12  8230  fodomr  9092  domssex  9102  fodomfir  9279  f1dmvrnfibi  9292  f1vrnfibi  9293  acndom  10004  acndom2  10007  ackbij1b  10191  fin1a2lem6  10358  hashf1dmrn  14408  cnt0  23233  cnt1  23237  cnhaus  23241  hmeoimaf1o  23657  uspgr1e  29171  s2f1  32866  lindflbs  33350  rankeq1o  36159  hfninf  36174  eldioph2lem2  42749