Theorem f1odm 6849

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

Syntax hints:   → wi 4   = wceq 1534  dom cdm 5684   Fn wfn 6551  –1-1-onto→wf1o 6555

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 395  df-fn 6559  df-f 6560  df-f1 6561  df-f1o 6563

This theorem is referenced by:  f1imacnv  6861  f1opw2  7683  xpcomco  9103  domss2  9177  mapen  9182  ssenen  9192  phplem2  9246  php3  9250  phplem4OLD  9258  php3OLD  9262  f1opwfi  9401  unxpwdom2  9632  cnfcomlem  9743  djuun  9970  ackbij2lem2  10283  ackbij2lem3  10284  fin4en1  10353  enfin2i  10365  gsumpropd2lem  18685  symgfixf1  19447  f1omvdmvd  19453  f1omvdconj  19456  pmtrfb  19475  symggen  19480  symggen2  19481  psgnunilem1  19503  basqtop  23706  reghmph  23788  nrmhmph  23789  indishmph  23793  ordthmeolem  23796  ufldom  23957  tgpconncompeqg  24107  imasf1oxms  24489  icchmeo  24956  icchmeoOLD  24957  dvcvx  26044  dvloglem  26672  f1ocnt  32707  cycpmconjvlem  33034  cycpmconjslem2  33048  madjusmdetlem2  33674  madjusmdetlem4  33676  tpr2rico  33758  ballotlemrv  34384  reprpmtf1o  34503  hgt750lemg  34531  subfacp1lem2b  35049  subfacp1lem5  35052  poimirlem3  37364  ismtyres  37549  eldioph2lem1  42484  lnmlmic  42816  ntrclsiex  43787  ntrneiiex  43810  ssnnf1octb  44867  f1oresf1o  46969  grimuhgr  47523