Theorem f1dm 6742

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

Syntax hints:   → wi 4   = wceq 1540  dom cdm 5631  –1-1→wf1 6496

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 6502  df-f 6503  df-f1 6504

This theorem is referenced by:  f1iun  7902  fnwelem  8087  tposf12  8207  fodomr  9069  domssex  9079  fodomfir  9255  f1dmvrnfibi  9268  f1vrnfibi  9269  acndom  9982  acndom2  9985  ackbij1b  10169  fin1a2lem6  10336  hashf1dmrn  14386  cnt0  23267  cnt1  23271  cnhaus  23275  hmeoimaf1o  23691  uspgr1e  29225  s2f1  32917  lindflbs  33344  rankeq1o  36153  hfninf  36168  eldioph2lem2  42743