Theorem f1dm 6788

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

Syntax hints:   → wi 4   = wceq 1541  dom cdm 5675  –1-1→wf1 6537

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 206  df-an 397  df-fn 6543  df-f 6544  df-f1 6545

This theorem is referenced by:  f1iun  7926  fnwelem  8113  tposf12  8232  fodomr  9124  domssex  9134  f1dmvrnfibi  9332  f1vrnfibi  9333  acndom  10042  acndom2  10045  ackbij1b  10230  fin1a2lem6  10396  hashf1dmrn  14399  cnt0  22841  cnt1  22845  cnhaus  22849  hmeoimaf1o  23265  uspgr1e  28490  s2f1  32098  lindflbs  32483  rankeq1o  35131  hfninf  35146  eldioph2lem2  41484