Theorem f1f 6719

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 6486	. 2 ⊢ (𝐹:𝐴–1-1→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹))
2	1	simplbi 497	1 ⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹:𝐴⟶𝐵)

Syntax hints:   → wi 4  ^◡ccnv 5615  Fun wfun 6475  ⟶wf 6477  –1-1→wf1 6478

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-f1 6486

This theorem is referenced by:  f1fn  6720  f1ss  6724  f1ssres  6726  f1co  6730  f1of  6763  dff1o5  6772  f1un  6783  fsnd  6806  f1cofveqaeq  7191  f1cofveqaeqALT  7192  2f1fvneq  7194  f1dom3el3dif  7203  f1cdmsn  7216  f1prex  7218  cocan1  7225  fvf1pr  7241  f1iun  7876  f1dmex  7889  f1o2ndf1  8052  oacomf1olem  8479  brdomg  8881  f1dom2g  8892  f1domg  8894  dom3d  8916  f1imaen2g  8937  2dom  8952  domdifsn  8973  xpdom2  8985  domunsncan  8990  dom0  9018  fodomr  9041  domss2  9049  domssex2  9050  f1domfi  9090  sucdom2  9112  f1finf1o  9157  infn0  9186  f1fi  9198  fodomfir  9212  oiexg  9421  hartogslem1  9428  infdifsn  9547  fseqenlem1  9915  fseqenlem2  9916  ac10ct  9925  acndom  9942  acndom2  9945  dfac12lem2  10036  dfac12lem3  10037  ackbij1  10128  fictb  10135  cfsmolem  10161  cfcoflem  10163  cfcof  10165  fin23lem17  10229  fin23lem32  10235  fin23lem39  10241  fin23lem41  10243  fin1a2lem6  10296  fin1a2lem7  10297  iundom2g  10431  alephreg  10473  canthnumlem  10539  canthwelem  10541  pwfseqlem1  10549  pwfseqlem5  10554  fvf1tp  13693  seqf1olem1  13948  hashf1rn  14259  hashimarn  14347  hashf1dmcdm  14351  hashf1lem1  14362  hashf1lem2  14363  cshf1  14717  setcmon  17994  injsubmefmnd  18805  odinf  19476  odcl2  19478  sylow1lem2  19512  gsumval3lem1  19818  gsumval3lem2  19819  gsumval3  19820  gsumzcl2  19823  gsumzf1o  19825  gsumzaddlem  19834  gsumzmhm  19850  gsumzoppg  19857  dprdf1  19948  f1lindf  21760  f1linds  21763  lindfmm  21765  mdetunilem8  22535  2ndcdisj  23372  itg1addlem4  25628  reeff1o  26385  birthdaylem1  26889  dchrisum0fno1  27450  ushgruhgr  29048  umgr0e  29089  usgredgss  29138  ausgrusgrb  29144  usgrss  29153  uspgrupgr  29157  usgrumgr  29160  usgruspgrb  29162  usgrislfuspgr  29166  usgredg2ALT  29172  ushgredgedg  29208  ushgredgedgloop  29210  usgr2pth  29743  0wlkons1  30099  trlsegvdeg  30205  fsumiunle  32810  cycpmco2lem1  33093  cycpmco2lem5  33097  cycpmco2  33100  cycpmconjv  33109  cyc3conja  33124  idomsubr  33273  islbs5  33343  extdgfialglem1  33703  qqhre  34031  esumiun  34105  erdszelem4  35236  erdszelem8  35240  erdszelem9  35241  erdsze2lem2  35246  pibt2  37457  aks6d1c2  42169  aks6d1c6lem3  42211  diophrw  42798  eldioph2lem2  42800  eldioph2  42801  eldioph2b  42802  dnwech  43087  cantnfub2  43361  seff  44348  fargshiftf1  47478  fmtnoinf  47573  upgrimtrlslem2  47942  ushggricedg  47964  grtrimap  47985  oppff1o  49187  fucoppcid  49446  diag1f1o  49572  diag2f1o  49575