Theorem f1odm 6822

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 6819	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → 𝐹 Fn 𝐴)
2		fndm 6641	. 2 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
3	1, 2	syl 17	1 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → dom 𝐹 = 𝐴)

Syntax hints:   → wi 4   = wceq 1540  dom cdm 5654   Fn wfn 6526  –1-1-onto→wf1o 6530

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 6534  df-f 6535  df-f1 6536  df-f1o 6538

This theorem is referenced by:  f1imacnv  6834  f1ounsn  7265  f1opw2  7662  xpcomco  9076  domss2  9150  mapen  9155  ssenen  9165  phplem2  9219  php3  9223  php3OLD  9233  f1opwfi  9368  unxpwdom2  9602  cnfcomlem  9713  djuun  9940  ackbij2lem2  10253  ackbij2lem3  10254  fin4en1  10323  enfin2i  10335  gsumpropd2lem  18657  symgfixf1  19418  f1omvdmvd  19424  f1omvdconj  19427  pmtrfb  19446  symggen  19451  symggen2  19452  psgnunilem1  19474  basqtop  23649  reghmph  23731  nrmhmph  23732  indishmph  23736  ordthmeolem  23739  ufldom  23900  tgpconncompeqg  24050  imasf1oxms  24428  icchmeo  24889  icchmeoOLD  24890  dvcvx  25977  dvloglem  26609  f1ocnt  32779  cycpmconjvlem  33152  cycpmconjslem2  33166  madjusmdetlem2  33859  madjusmdetlem4  33861  tpr2rico  33943  ballotlemrv  34552  reprpmtf1o  34658  hgt750lemg  34686  subfacp1lem2b  35203  subfacp1lem5  35206  poimirlem3  37647  ismtyres  37832  eldioph2lem1  42783  lnmlmic  43112  ntrclsiex  44077  ntrneiiex  44100  ssnnf1octb  45218  f1oresf1o  47319  grimuhgr  47900  isubgr3stgrlem3  47980