Theorem f1dm 6732

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

Syntax hints:   → wi 4   = wceq 1542  dom cdm 5622  –1-1→wf1 6487

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 6493  df-f 6494  df-f1 6495

This theorem is referenced by:  f1iun  7888  fnwelem  8072  tposf12  8192  fodomr  9057  domssex  9067  fodomfir  9229  f1dmvrnfibi  9242  f1vrnfibi  9243  acndom  9962  acndom2  9965  ackbij1b  10149  fin1a2lem6  10316  hashf1dmrn  14367  cnt0  23289  cnt1  23293  cnhaus  23297  hmeoimaf1o  23713  uspgr1e  29301  s2f1  33010  lindflbs  33444  fineqvinfep  35275  rankeq1o  36359  hfninf  36374  eldioph2lem2  43192