Theorem f1dm 5790

Description: The domain of a one-to-one mapping. (Contributed by NM, 8-Mar-2014.)

Assertion

Ref	Expression
f1dm

Proof of Theorem f1dm

Step	Hyp	Ref	Expression
1		f1fn 5787	. 2
2		fndm 5685	. 2
3	1, 2	syl 16	1

Syntax hints:  ->wi 4  =wceq 1395  domcdm 5004  Fnwfn 5588  -1-1->wf1 5590

This theorem is referenced by:  fun11iun  6760  fnwelem  6915  tposf12  6999  fodomr  7688  domssex  7698  acndom  8453  acndom2  8456  ackbij1b  8640  fin1a2lem6  8806  cnt0  19847  cnt1  19851  cnhaus  19855  hmeoimaf1o  20271  uslgra1  24372  usgra1  24373  ctex  27531  rankeq1o  29828  hfninf  29843  eldioph2lem2  30694  f1dmvrnfibi  32312  f1vrnfibi  32313

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 185  df-an 371  df-fn 5596  df-f 5597  df-f1 5598