Theorem f1dm 6806

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 6801	. 2 ⊢ (𝐹:𝐴⟶1-1𝐵 → 𝐹 Fn 𝐴)
2	1	fndmd 6666	1 ⊢ (𝐹:𝐴⟶1-1𝐵 → dom 𝐹 = 𝐴)

This proof depends on syntax axioms:   → wi 4   = wceq 1570  dom cdm 5655  ⟶1-1wf1 6555

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-fn 6561  df-f 6562  df-f1 6563

This theorem is used by:  f1iun  7980  fnwelem  8170  tposf12  8296  fodomr  9175  domssex  9185  fodomfir  9347  f1dmvrnfibi  9358  f1vrnfibi  9359  acndom  10157  acndom2  10160  ackbij1b  10343  fin1a2lem6  10510  hashf1dmrn  14615  cnt0  23694  cnt1  23698  cnhaus  23702  hmeoimaf1o  24119  uspgr1e  29855  s2f1  33580  lindflbs  34004  fineqvinfep  35893  vonf1wev  36036  eldioph2lem2  43965