Theorem f1odm 6775

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

Syntax hints:   → wi 4   = wceq 1541  dom cdm 5621   Fn wfn 6484  –1-1-onto→wf1o 6488

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 6492  df-f 6493  df-f1 6494  df-f1o 6496

This theorem is referenced by:  f1imacnv  6787  f1ounsn  7215  f1opw2  7610  xpcomco  8990  domss2  9059  mapen  9064  ssenen  9074  phplem2  9124  php3  9128  f1opwfi  9250  unxpwdom2  9484  cnfcomlem  9599  djuun  9829  ackbij2lem2  10140  ackbij2lem3  10141  fin4en1  10210  enfin2i  10222  gsumpropd2lem  18597  symgfixf1  19359  f1omvdmvd  19365  f1omvdconj  19368  pmtrfb  19387  symggen  19392  symggen2  19393  psgnunilem1  19415  basqtop  23636  reghmph  23718  nrmhmph  23719  indishmph  23723  ordthmeolem  23726  ufldom  23887  tgpconncompeqg  24037  imasf1oxms  24414  icchmeo  24875  icchmeoOLD  24876  dvcvx  25962  dvloglem  26594  f1ocnt  32793  cycpmconjvlem  33121  cycpmconjslem2  33135  madjusmdetlem2  33852  madjusmdetlem4  33854  tpr2rico  33936  ballotlemrv  34544  reprpmtf1o  34650  hgt750lemg  34678  vonf1owev  35163  subfacp1lem2b  35236  subfacp1lem5  35239  poimirlem3  37673  ismtyres  37858  eldioph2lem1  42867  lnmlmic  43195  ntrclsiex  44160  ntrneiiex  44183  ssnnf1octb  45305  f1oresf1o  47404  grimuhgr  48001  isubgr3stgrlem3  48082