Theorem f1odm 6852

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

Syntax hints:   → wi 4   = wceq 1540  dom cdm 5685   Fn wfn 6556  –1-1-onto→wf1o 6560

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 6564  df-f 6565  df-f1 6566  df-f1o 6568

This theorem is referenced by:  f1imacnv  6864  f1ounsn  7292  f1opw2  7688  xpcomco  9102  domss2  9176  mapen  9181  ssenen  9191  phplem2  9245  php3  9249  phplem4OLD  9257  php3OLD  9261  f1opwfi  9396  unxpwdom2  9628  cnfcomlem  9739  djuun  9966  ackbij2lem2  10279  ackbij2lem3  10280  fin4en1  10349  enfin2i  10361  gsumpropd2lem  18692  symgfixf1  19455  f1omvdmvd  19461  f1omvdconj  19464  pmtrfb  19483  symggen  19488  symggen2  19489  psgnunilem1  19511  basqtop  23719  reghmph  23801  nrmhmph  23802  indishmph  23806  ordthmeolem  23809  ufldom  23970  tgpconncompeqg  24120  imasf1oxms  24502  icchmeo  24971  icchmeoOLD  24972  dvcvx  26059  dvloglem  26690  f1ocnt  32804  cycpmconjvlem  33161  cycpmconjslem2  33175  madjusmdetlem2  33827  madjusmdetlem4  33829  tpr2rico  33911  ballotlemrv  34522  reprpmtf1o  34641  hgt750lemg  34669  subfacp1lem2b  35186  subfacp1lem5  35189  poimirlem3  37630  ismtyres  37815  eldioph2lem1  42771  lnmlmic  43100  ntrclsiex  44066  ntrneiiex  44089  ssnnf1octb  45199  f1oresf1o  47302  grimuhgr  47878  isubgr3stgrlem3  47935