Theorem f1dm 6724

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

Syntax hints:   → wi 4   = wceq 1540  dom cdm 5619  –1-1→wf1 6479

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 6485  df-f 6486  df-f1 6487

This theorem is referenced by:  f1iun  7879  fnwelem  8064  tposf12  8184  fodomr  9045  domssex  9055  fodomfir  9218  f1dmvrnfibi  9231  f1vrnfibi  9232  acndom  9945  acndom2  9948  ackbij1b  10132  fin1a2lem6  10299  hashf1dmrn  14350  cnt0  23231  cnt1  23235  cnhaus  23239  hmeoimaf1o  23655  uspgr1e  29193  s2f1  32895  lindflbs  33325  rankeq1o  36165  hfninf  36180  eldioph2lem2  42754