Theorem f1dm 6780

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

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

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 401  df-fn 6539  df-f 6540  df-f1 6541

This theorem is used by:  f1iun  7939  fnwelem  8125  tposf12  8245  fodomr  9114  domssex  9124  fodomfir  9285  f1dmvrnfibi  9296  f1vrnfibi  9297  acndom  10042  acndom2  10045  ackbij1b  10228  fin1a2lem6  10395  hashf1dmrn  14487  cnt0  23514  cnt1  23518  cnhaus  23522  hmeoimaf1o  23938  uspgr1e  29605  s2f1  33275  lindflbs  33701  fineqvinfep  35546  vonf1wev  35600  rankeq1o  36671  hfninf  36686  eldioph2lem2  43520