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 𝐹 = 𝐴)

Syntax hints:   → wi 4   = wceq 1568  dom cdm 5661  –1-1→wf1 6533

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

This theorem is referenced by:  f1iun  7940  fnwelem  8126  tposf12  8246  fodomr  9115  domssex  9125  fodomfir  9286  f1dmvrnfibi  9297  f1vrnfibi  9298  acndom  10034  acndom2  10037  ackbij1b  10220  fin1a2lem6  10388  hashf1dmrn  14479  cnt0  23482  cnt1  23486  cnhaus  23490  hmeoimaf1o  23906  uspgr1e  29560  s2f1  33231  lindflbs  33658  fineqvinfep  35492  vonf1wev  35546  rankeq1o  36617  hfninf  36632  eldioph2lem2  43440