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  9980  acndom2  9983  ackbij1b  10167  fin1a2lem6  10334  hashf1dmrn  14384  cnt0  23266  cnt1  23270  cnhaus  23274  hmeoimaf1o  23690  uspgr1e  29224  s2f1  32916  lindflbs  33343  rankeq1o  36152  hfninf  36167  eldioph2lem2  42742