Theorem f1dm 6730

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

Syntax hints:   → wi 4   = wceq 1548  dom cdm 5620  –1-1→wf1 6485

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 209  df-an 398  df-fn 6491  df-f 6492  df-f1 6493

This theorem is referenced by:  f1iun  7888  fnwelem  8073  tposf12  8193  fodomr  9060  domssex  9070  fodomfir  9232  f1dmvrnfibi  9245  f1vrnfibi  9246  acndom  9968  acndom2  9971  ackbij1b  10155  fin1a2lem6  10323  hashf1dmrn  14400  cnt0  23332  cnt1  23336  cnhaus  23340  hmeoimaf1o  23756  uspgr1e  29333  s2f1  33026  lindflbs  33464  fineqvinfep  35319  rankeq1o  36412  hfninf  36427  eldioph2lem2  43223