Theorem f1dm 6733

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

Syntax hints:   → wi 4   = wceq 1542  dom cdm 5623  –1-1→wf1 6488

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 6494  df-f 6495  df-f1 6496

This theorem is referenced by:  f1iun  7888  fnwelem  8073  tposf12  8193  fodomr  9058  domssex  9068  fodomfir  9230  f1dmvrnfibi  9243  f1vrnfibi  9244  acndom  9963  acndom2  9966  ackbij1b  10150  fin1a2lem6  10317  hashf1dmrn  14368  cnt0  23292  cnt1  23296  cnhaus  23300  hmeoimaf1o  23716  uspgr1e  29298  s2f1  33006  lindflbs  33439  fineqvinfep  35260  rankeq1o  36344  hfninf  36359  eldioph2lem2  43040