Theorem f1odm 6866

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

Syntax hints:   → wi 4   = wceq 1537  dom cdm 5700   Fn wfn 6568  –1-1-onto→wf1o 6572

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 6576  df-f 6577  df-f1 6578  df-f1o 6580

This theorem is referenced by:  f1imacnv  6878  f1opw2  7705  xpcomco  9128  domss2  9202  mapen  9207  ssenen  9217  phplem2  9271  php3  9275  phplem4OLD  9283  php3OLD  9287  f1opwfi  9426  unxpwdom2  9657  cnfcomlem  9768  djuun  9995  ackbij2lem2  10308  ackbij2lem3  10309  fin4en1  10378  enfin2i  10390  gsumpropd2lem  18717  symgfixf1  19479  f1omvdmvd  19485  f1omvdconj  19488  pmtrfb  19507  symggen  19512  symggen2  19513  psgnunilem1  19535  basqtop  23740  reghmph  23822  nrmhmph  23823  indishmph  23827  ordthmeolem  23830  ufldom  23991  tgpconncompeqg  24141  imasf1oxms  24523  icchmeo  24990  icchmeoOLD  24991  dvcvx  26079  dvloglem  26708  f1ocnt  32807  cycpmconjvlem  33134  cycpmconjslem2  33148  madjusmdetlem2  33774  madjusmdetlem4  33776  tpr2rico  33858  ballotlemrv  34484  reprpmtf1o  34603  hgt750lemg  34631  subfacp1lem2b  35149  subfacp1lem5  35152  poimirlem3  37583  ismtyres  37768  eldioph2lem1  42716  lnmlmic  43045  ntrclsiex  44015  ntrneiiex  44038  ssnnf1octb  45101  f1oresf1o  47205  grimuhgr  47762