Theorem f1dm 6321

Description: The domain of a one-to-one mapping. (Contributed by NM, 8-Mar-2014.)

Assertion

Ref	Expression
f1dm	⊢ (𝐹:𝐴–1-1→𝐵 → dom 𝐹 = 𝐴)

Proof of Theorem f1dm

Step	Hyp	Ref	Expression
1		f1fn 6318	. 2 ⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹 Fn 𝐴)
2		fndm 6202	. 2 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
3	1, 2	syl 17	1 ⊢ (𝐹:𝐴–1-1→𝐵 → dom 𝐹 = 𝐴)

Syntax hints:   → wi 4   = wceq 1653  dom cdm 5313   Fn wfn 6097  –1-1→wf1 6099

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 199  df-an 386  df-fn 6105  df-f 6106  df-f1 6107

This theorem is referenced by:  fun11iun  7362  fnwelem  7530  tposf12  7616  ctex  8211  fodomr  8354  domssex  8364  f1dmvrnfibi  8493  f1vrnfibi  8494  acndom  9161  acndom2  9164  ackbij1b  9350  fin1a2lem6  9516  cnt0  21478  cnt1  21482  cnhaus  21486  hmeoimaf1o  21901  uspgr1e  26477  rankeq1o  32790  hfninf  32805  eldioph2lem2  38105