Theorem f1odm 6786

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

Syntax hints:   → wi 4   = wceq 1542  dom cdm 5632   Fn wfn 6495  –1-1-onto→wf1o 6499

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 6503  df-f 6504  df-f1 6505  df-f1o 6507

This theorem is referenced by:  f1imacnv  6798  f1ounsn  7228  f1opw2  7623  xpcomco  9007  domss2  9076  mapen  9081  ssenen  9091  phplem2  9141  php3  9145  f1opwfi  9268  unxpwdom2  9505  cnfcomlem  9620  djuun  9850  ackbij2lem2  10161  ackbij2lem3  10162  fin4en1  10231  enfin2i  10243  gsumpropd2lem  18616  symgfixf1  19378  f1omvdmvd  19384  f1omvdconj  19387  pmtrfb  19406  symggen  19411  symggen2  19412  psgnunilem1  19434  basqtop  23667  reghmph  23749  nrmhmph  23750  indishmph  23754  ordthmeolem  23757  ufldom  23918  tgpconncompeqg  24068  imasf1oxms  24445  icchmeo  24906  icchmeoOLD  24907  dvcvx  25993  dvloglem  26625  f1ocnt  32890  cycpmconjvlem  33234  cycpmconjslem2  33248  madjusmdetlem2  34005  madjusmdetlem4  34007  tpr2rico  34089  ballotlemrv  34697  reprpmtf1o  34803  hgt750lemg  34831  vonf1owev  35321  subfacp1lem2b  35394  subfacp1lem5  35397  poimirlem3  37871  ismtyres  38056  eldioph2lem1  43114  lnmlmic  43442  ntrclsiex  44406  ntrneiiex  44429  ssnnf1octb  45550  f1oresf1o  47647  grimuhgr  48244  isubgr3stgrlem3  48325