Theorem f1f 6781

Description: A one-to-one mapping is a mapping. (Contributed by NM, 31-Dec-1996.)

Assertion

Ref	Expression
f1f	⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹:𝐴⟶𝐵)

Proof of Theorem f1f

Step	Hyp	Ref	Expression
1		df-f1 6548	. 2 ⊢ (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹))
2	1	simplbi 502	1 ⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹:𝐴⟶𝐵)

This proof depends on syntax axioms:   → wi 4  ^◡ccnv 5665  Fun wfun 6537  ⟶wf 6539  –1-1→wf1 6540

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-f1 6548

This theorem is used by:  f1fn  6782  f1rel  6785  f1ss  6788  f1ssres  6790  f1co  6794  f1of  6827  dff1o5  6837  f1un  6848  fsnd  6872  f1cofveqaeq  7262  f1cofveqaeqALT  7263  2f1fvneq  7265  f1dom3el3dif  7274  f1cdmsn  7291  f1prex  7293  cocan1  7300  fvf1pr  7316  f1we  7364  f1iun  7950  f1dmex  7963  f1o2ndf1  8126  oacomf1olem  8558  brdomg  8964  f1dom2g  8975  f1domg  8977  dom3d  9000  f1imaen2g  9021  2dom  9037  domdifsn  9058  xpdom2  9070  domunsncan  9075  dom0  9103  fodomr  9126  domss2  9134  domssex2  9135  f1domfi  9175  sucdom2  9197  f1finf1o  9243  infn0  9272  f1fi  9284  fodomfir  9297  oiexg  9507  hartogslem1  9514  infdifsn  9636  fseqenlem1  10027  fseqenlem2  10028  acndom  10054  acndom2  10057  dfac12lem2  10147  dfac12lem3  10148  ackbij1  10239  fictb  10246  cfsmolem  10272  cfcoflem  10274  cfcof  10276  fin23lem17  10340  fin23lem32  10346  fin23lem39  10352  fin23lem41  10354  fin1a2lem6  10407  fin1a2lem7  10408  iundom2g  10542  alephreg  10585  canthnumlem  10651  canthwelem  10653  pwfseqlem1  10661  pwfseqlem5  10666  fvf1tp  13842  seqf1olem1  14097  hashf1rn  14408  hashimarn  14497  hashf1dmcdm  14501  hashf1lem1  14512  hashf1lem2  14513  cshf1  14873  setcmon  18169  injsubmefmnd  18987  odinf  19664  odcl2  19666  sylow1lem2  19700  gsumval3lem1  20006  gsumval3lem2  20007  gsumval3  20008  gsumzcl2  20011  gsumzf1o  20013  gsumzaddlem  20022  gsumzmhm  20038  gsumzoppg  20045  dprdf1  20136  f1lindf  22009  f1linds  22012  lindfmm  22014  mdetunilem8  22813  2ndcdisj  23650  itg1addlem4  25895  reeff1o  26647  birthdaylem1  27153  dchrisum0fno1  27712  ushgruhgr  29456  umgr0e  29497  usgredgss  29546  ausgrusgrb  29552  usgrss  29561  uspgrupgr  29565  usgrumgr  29568  usgruspgrb  29570  usgrislfuspgr  29574  usgredg2ALT  29580  ushgredgedg  29616  ushgredgedgloop  29618  usgr2pth  30150  0wlkons1  30509  trlsegvdeg  30615  fsumiunle  33210  cycpmco2lem1  33477  cycpmco2lem5  33481  cycpmco2  33484  cycpmconjv  33493  cyc3conja  33508  idomsubr  33661  islbs5  33724  extdgfialglem1  34113  qqhre  34441  esumiun  34515  vonf1wev  35616  erdszelem4  35707  erdszelem8  35711  erdszelem9  35712  erdsze2lem2  35717  mh-inf3f1  37093  pibt2  38104  aks6d1c2  42938  aks6d1c6lem3  42980  diophrw  43531  eldioph2lem2  43533  eldioph2  43534  eldioph2b  43535  cantnfub2  44090  seff  45060  fargshiftf1  48231  fmtnoinf  48329  upgrimtrlslem2  48711  ushggricedg  48733  grtrimap  48754  oppff1o  49968  fucoppcid  50227  diag1f1o  50353  diag2f1o  50356