Theorem f1dm 6729

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

Syntax hints:   → wi 4   = wceq 1542  dom cdm 5620  –1-1→wf1 6484

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 6490  df-f 6491  df-f1 6492

This theorem is referenced by:  f1iun  7886  fnwelem  8070  tposf12  8190  fodomr  9055  domssex  9065  fodomfir  9227  f1dmvrnfibi  9240  f1vrnfibi  9241  acndom  9962  acndom2  9965  ackbij1b  10149  fin1a2lem6  10316  hashf1dmrn  14394  cnt0  23299  cnt1  23303  cnhaus  23307  hmeoimaf1o  23723  uspgr1e  29301  s2f1  32993  lindflbs  33427  fineqvinfep  35257  rankeq1o  36341  hfninf  36356  eldioph2lem2  43181