Theorem f1dm 6784

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569  dom cdm 5650  –1-1→wf1 6535

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-fn 6541  df-f 6542  df-f1 6543

This theorem is used by:  f1iun  7956  fnwelem  8143  tposf12  8268  fodomr  9147  domssex  9157  fodomfir  9319  f1dmvrnfibi  9330  f1vrnfibi  9331  acndom  10130  acndom2  10133  ackbij1b  10316  fin1a2lem6  10483  hashf1dmrn  14588  cnt0  23664  cnt1  23668  cnhaus  23672  hmeoimaf1o  24089  uspgr1e  29825  s2f1  33552  lindflbs  33976  fineqvinfep  35835  vonf1wev  35929  eldioph2lem2  43815