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 1541  dom cdm 5619  –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  7882  fnwelem  8067  tposf12  8187  fodomr  9047  domssex  9057  fodomfir  9218  f1dmvrnfibi  9231  f1vrnfibi  9232  acndom  9948  acndom2  9951  ackbij1b  10135  fin1a2lem6  10302  hashf1dmrn  14356  cnt0  23267  cnt1  23271  cnhaus  23275  hmeoimaf1o  23691  uspgr1e  29229  s2f1  32933  lindflbs  33351  rankeq1o  36222  hfninf  36237  eldioph2lem2  42859