Theorem f1odm 6838

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

Syntax hints:   → wi 4   = wceq 1542  dom cdm 5677   Fn wfn 6539  –1-1-onto→wf1o 6543

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 398  df-fn 6547  df-f 6548  df-f1 6549  df-f1o 6551

This theorem is referenced by:  f1imacnv  6850  f1opw2  7661  xpcomco  9062  domss2  9136  mapen  9141  ssenen  9151  phplem2  9208  php3  9212  phplem4OLD  9220  php3OLD  9224  f1opwfi  9356  unxpwdom2  9583  cnfcomlem  9694  djuun  9921  ackbij2lem2  10235  ackbij2lem3  10236  fin4en1  10304  enfin2i  10316  hashfacenOLD  14414  gsumpropd2lem  18598  symgfixf1  19305  f1omvdmvd  19311  f1omvdconj  19314  pmtrfb  19333  symggen  19338  symggen2  19339  psgnunilem1  19361  basqtop  23215  reghmph  23297  nrmhmph  23298  indishmph  23302  ordthmeolem  23305  ufldom  23466  tgpconncompeqg  23616  imasf1oxms  23998  icchmeo  24457  dvcvx  25537  dvloglem  26156  f1ocnt  32013  cycpmconjvlem  32300  cycpmconjslem2  32314  madjusmdetlem2  32808  madjusmdetlem4  32810  tpr2rico  32892  ballotlemrv  33518  reprpmtf1o  33638  hgt750lemg  33666  subfacp1lem2b  34172  subfacp1lem5  34175  gg-icchmeo  35170  poimirlem3  36491  ismtyres  36676  eldioph2lem1  41498  lnmlmic  41830  ntrclsiex  42804  ntrneiiex  42827  ssnnf1octb  43893  f1oresf1o  45998