Theorem f1odm 6054

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

Syntax hints:   → wi 4   = wceq 1475  dom cdm 5038   Fn wfn 5799  –1-1-onto→wf1o 5803

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 196  df-an 385  df-fn 5807  df-f 5808  df-f1 5809  df-f1o 5811

This theorem is referenced by:  f1imacnv  6066  f1opw2  6786  xpcomco  7935  domss2  8004  mapen  8009  ssenen  8019  phplem4  8027  php3  8031  f1opwfi  8153  unxpwdom2  8376  cnfcomlem  8479  ackbij2lem2  8945  ackbij2lem3  8946  fin4en1  9014  enfin2i  9026  hashfacen  13095  gsumpropd2lem  17096  symgbas  17623  symgfixf1  17680  f1omvdmvd  17686  f1omvdconj  17689  pmtrfb  17708  symggen  17713  symggen2  17714  psgnunilem1  17736  basqtop  21324  reghmph  21406  nrmhmph  21407  indishmph  21411  ordthmeolem  21414  ufldom  21576  tgpconcompeqg  21725  imasf1oxms  22104  icchmeo  22548  dvcvx  23587  dvloglem  24194  f1ocnt  28946  madjusmdetlem2  29222  madjusmdetlem4  29224  tpr2rico  29286  ballotlemrv  29908  subfacp1lem2b  30417  subfacp1lem5  30420  poimirlem3  32582  ismtyres  32777  eldioph2lem1  36341  lnmlmic  36676  ntrclsiex  37371  ntrneiiex  37394  ssnnf1octb  38377