Theorem f1f 6730

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

Syntax hints:   → wi 4  ^◡ccnv 5623  Fun wfun 6486  ⟶wf 6488  –1-1→wf1 6489

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 6497

This theorem is referenced by:  f1fn  6731  f1ss  6735  f1ssres  6737  f1co  6741  f1of  6774  dff1o5  6783  f1un  6794  fsnd  6818  f1cofveqaeq  7205  f1cofveqaeqALT  7206  2f1fvneq  7208  f1dom3el3dif  7217  f1cdmsn  7230  f1prex  7232  cocan1  7239  fvf1pr  7255  f1iun  7890  f1dmex  7903  f1o2ndf1  8065  oacomf1olem  8492  brdomg  8898  f1dom2g  8909  f1domg  8911  dom3d  8934  f1imaen2g  8955  2dom  8970  domdifsn  8991  xpdom2  9003  domunsncan  9008  dom0  9036  fodomr  9059  domss2  9067  domssex2  9068  f1domfi  9108  sucdom2  9130  f1finf1o  9176  infn0  9205  f1fi  9217  fodomfir  9231  oiexg  9443  hartogslem1  9450  infdifsn  9569  fseqenlem1  9937  fseqenlem2  9938  ac10ct  9947  acndom  9964  acndom2  9967  dfac12lem2  10058  dfac12lem3  10059  ackbij1  10150  fictb  10157  cfsmolem  10183  cfcoflem  10185  cfcof  10187  fin23lem17  10251  fin23lem32  10257  fin23lem39  10263  fin23lem41  10265  fin1a2lem6  10318  fin1a2lem7  10319  iundom2g  10453  alephreg  10496  canthnumlem  10562  canthwelem  10564  pwfseqlem1  10572  pwfseqlem5  10577  fvf1tp  13739  seqf1olem1  13994  hashf1rn  14305  hashimarn  14393  hashf1dmcdm  14397  hashf1lem1  14408  hashf1lem2  14409  cshf1  14763  setcmon  18045  injsubmefmnd  18856  odinf  19529  odcl2  19531  sylow1lem2  19565  gsumval3lem1  19871  gsumval3lem2  19872  gsumval3  19873  gsumzcl2  19876  gsumzf1o  19878  gsumzaddlem  19887  gsumzmhm  19903  gsumzoppg  19910  dprdf1  20001  f1lindf  21812  f1linds  21815  lindfmm  21817  mdetunilem8  22594  2ndcdisj  23431  itg1addlem4  25676  reeff1o  26425  birthdaylem1  26928  dchrisum0fno1  27488  ushgruhgr  29152  umgr0e  29193  usgredgss  29242  ausgrusgrb  29248  usgrss  29257  uspgrupgr  29261  usgrumgr  29264  usgruspgrb  29266  usgrislfuspgr  29270  usgredg2ALT  29276  ushgredgedg  29312  ushgredgedgloop  29314  usgr2pth  29847  0wlkons1  30206  trlsegvdeg  30312  fsumiunle  32917  cycpmco2lem1  33202  cycpmco2lem5  33206  cycpmco2  33209  cycpmconjv  33218  cyc3conja  33233  idomsubr  33385  islbs5  33455  extdgfialglem1  33852  qqhre  34180  esumiun  34254  erdszelem4  35392  erdszelem8  35396  erdszelem9  35397  erdsze2lem2  35402  mh-inf3f1  36739  pibt2  37747  aks6d1c2  42583  aks6d1c6lem3  42625  diophrw  43205  eldioph2lem2  43207  eldioph2  43208  eldioph2b  43209  dnwech  43494  cantnfub2  43768  seff  44754  fargshiftf1  47913  fmtnoinf  48011  upgrimtrlslem2  48393  ushggricedg  48415  grtrimap  48436  oppff1o  49636  fucoppcid  49895  diag1f1o  50021  diag2f1o  50024