Theorem f1dm 6808

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

Syntax hints:   → wi 4   = wceq 1540  dom cdm 5685  –1-1→wf1 6558

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 6564  df-f 6565  df-f1 6566

This theorem is referenced by:  f1iun  7968  fnwelem  8156  tposf12  8276  fodomr  9168  domssex  9178  fodomfir  9368  f1dmvrnfibi  9381  f1vrnfibi  9382  acndom  10091  acndom2  10094  ackbij1b  10278  fin1a2lem6  10445  hashf1dmrn  14482  cnt0  23354  cnt1  23358  cnhaus  23362  hmeoimaf1o  23778  uspgr1e  29261  s2f1  32929  lindflbs  33407  rankeq1o  36172  hfninf  36187  eldioph2lem2  42772