Theorem f1dm 6778

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

Syntax hints:   → wi 4   = wceq 1540  dom cdm 5654  –1-1→wf1 6528

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 6534  df-f 6535  df-f1 6536

This theorem is referenced by:  f1iun  7942  fnwelem  8130  tposf12  8250  fodomr  9142  domssex  9152  fodomfir  9340  f1dmvrnfibi  9353  f1vrnfibi  9354  acndom  10065  acndom2  10068  ackbij1b  10252  fin1a2lem6  10419  hashf1dmrn  14461  cnt0  23284  cnt1  23288  cnhaus  23292  hmeoimaf1o  23708  uspgr1e  29223  s2f1  32920  lindflbs  33394  rankeq1o  36189  hfninf  36204  eldioph2lem2  42784