Theorem f1odm 6778

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

Assertion

Ref	Expression
f1odm	⊢ (𝐹:𝐴–1-1-onto→𝐵 → dom 𝐹 = 𝐴)

Proof of Theorem f1odm

Step	Hyp	Ref	Expression
1		f1ofn 6775	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → 𝐹 Fn 𝐴)
2		fndm 6595	. 2 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
3	1, 2	syl 17	1 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → dom 𝐹 = 𝐴)

Syntax hints:   → wi 4   = wceq 1542  dom cdm 5624   Fn wfn 6487  –1-1-onto→wf1o 6491

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 207  df-an 396  df-fn 6495  df-f 6496  df-f1 6497  df-f1o 6499

This theorem is referenced by:  f1imacnv  6790  f1ounsn  7220  f1opw2  7615  xpcomco  8998  domss2  9067  mapen  9072  ssenen  9082  phplem2  9132  php3  9136  f1opwfi  9259  unxpwdom2  9496  cnfcomlem  9611  djuun  9841  ackbij2lem2  10152  ackbij2lem3  10153  fin4en1  10222  enfin2i  10234  gsumpropd2lem  18638  symgfixf1  19403  f1omvdmvd  19409  f1omvdconj  19412  pmtrfb  19431  symggen  19436  symggen2  19437  psgnunilem1  19459  basqtop  23686  reghmph  23768  nrmhmph  23769  indishmph  23773  ordthmeolem  23776  ufldom  23937  tgpconncompeqg  24087  imasf1oxms  24464  icchmeo  24918  dvcvx  25997  dvloglem  26625  f1ocnt  32888  cycpmconjvlem  33217  cycpmconjslem2  33231  madjusmdetlem2  33988  madjusmdetlem4  33990  tpr2rico  34072  ballotlemrv  34680  reprpmtf1o  34786  hgt750lemg  34814  vonf1owev  35306  subfacp1lem2b  35379  subfacp1lem5  35382  poimirlem3  37958  ismtyres  38143  eldioph2lem1  43206  lnmlmic  43534  ntrclsiex  44498  ntrneiiex  44521  ssnnf1octb  45642  f1oresf1o  47750  grimuhgr  48375  isubgr3stgrlem3  48456