Theorem f1dm 6738

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

Syntax hints:   → wi 4   = wceq 1542  dom cdm 5628  –1-1→wf1 6493

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 6499  df-f 6500  df-f1 6501

This theorem is referenced by:  f1iun  7894  fnwelem  8078  tposf12  8198  fodomr  9063  domssex  9073  fodomfir  9235  f1dmvrnfibi  9248  f1vrnfibi  9249  acndom  9970  acndom2  9973  ackbij1b  10157  fin1a2lem6  10324  hashf1dmrn  14402  cnt0  23308  cnt1  23312  cnhaus  23316  hmeoimaf1o  23732  uspgr1e  29310  s2f1  33002  lindflbs  33436  fineqvinfep  35266  rankeq1o  36350  hfninf  36365  eldioph2lem2  43190