Theorem f1dm 6791

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

Syntax hints:   → wi 4   = wceq 1534  dom cdm 5672  –1-1→wf1 6539

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 396  df-fn 6545  df-f 6546  df-f1 6547

This theorem is referenced by:  f1iun  7941  fnwelem  8130  tposf12  8250  fodomr  9144  domssex  9154  f1dmvrnfibi  9352  f1vrnfibi  9353  acndom  10066  acndom2  10069  ackbij1b  10254  fin1a2lem6  10420  hashf1dmrn  14426  cnt0  23237  cnt1  23241  cnhaus  23245  hmeoimaf1o  23661  uspgr1e  29044  s2f1  32650  lindflbs  33034  rankeq1o  35703  hfninf  35718  eldioph2lem2  42103