Theorem f1dm 6781

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570  dom cdm 5659  –1-1→wf1 6534

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 6540  df-f 6541  df-f1 6542

This theorem is used by:  f1iun  7944  fnwelem  8132  tposf12  8252  fodomr  9129  domssex  9139  fodomfir  9300  f1dmvrnfibi  9311  f1vrnfibi  9312  acndom  10057  acndom2  10060  ackbij1b  10243  fin1a2lem6  10410  hashf1dmrn  14510  cnt0  23572  cnt1  23576  cnhaus  23580  hmeoimaf1o  23997  uspgr1e  29690  s2f1  33376  lindflbs  33799  fineqvinfep  35638  vonf1wev  35692  rankeq1o  36738  hfninf  36753  eldioph2lem2  43593