Theorem f1f 6736

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

Syntax hints:   → wi 4  ^◡ccnv 5630  Fun wfun 6492  ⟶wf 6494  –1-1→wf1 6495

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 6503

This theorem is referenced by:  f1fn  6737  f1ss  6741  f1ssres  6743  f1co  6747  f1of  6780  dff1o5  6789  f1un  6800  fsnd  6824  f1cofveqaeq  7212  f1cofveqaeqALT  7213  2f1fvneq  7215  f1dom3el3dif  7224  f1cdmsn  7237  f1prex  7239  cocan1  7246  fvf1pr  7262  f1iun  7897  f1dmex  7910  f1o2ndf1  8072  oacomf1olem  8499  brdomg  8905  f1dom2g  8916  f1domg  8918  dom3d  8941  f1imaen2g  8962  2dom  8977  domdifsn  8998  xpdom2  9010  domunsncan  9015  dom0  9043  fodomr  9066  domss2  9074  domssex2  9075  f1domfi  9115  sucdom2  9137  f1finf1o  9183  infn0  9212  f1fi  9224  fodomfir  9238  oiexg  9450  hartogslem1  9457  infdifsn  9578  fseqenlem1  9946  fseqenlem2  9947  ac10ct  9956  acndom  9973  acndom2  9976  dfac12lem2  10067  dfac12lem3  10068  ackbij1  10159  fictb  10166  cfsmolem  10192  cfcoflem  10194  cfcof  10196  fin23lem17  10260  fin23lem32  10266  fin23lem39  10272  fin23lem41  10274  fin1a2lem6  10327  fin1a2lem7  10328  iundom2g  10462  alephreg  10505  canthnumlem  10571  canthwelem  10573  pwfseqlem1  10581  pwfseqlem5  10586  fvf1tp  13748  seqf1olem1  14003  hashf1rn  14314  hashimarn  14402  hashf1dmcdm  14406  hashf1lem1  14417  hashf1lem2  14418  cshf1  14772  setcmon  18054  injsubmefmnd  18865  odinf  19538  odcl2  19540  sylow1lem2  19574  gsumval3lem1  19880  gsumval3lem2  19881  gsumval3  19882  gsumzcl2  19885  gsumzf1o  19887  gsumzaddlem  19896  gsumzmhm  19912  gsumzoppg  19919  dprdf1  20010  f1lindf  21802  f1linds  21805  lindfmm  21807  mdetunilem8  22584  2ndcdisj  23421  itg1addlem4  25666  reeff1o  26412  birthdaylem1  26915  dchrisum0fno1  27474  ushgruhgr  29138  umgr0e  29179  usgredgss  29228  ausgrusgrb  29234  usgrss  29243  uspgrupgr  29247  usgrumgr  29250  usgruspgrb  29252  usgrislfuspgr  29256  usgredg2ALT  29262  ushgredgedg  29298  ushgredgedgloop  29300  usgr2pth  29832  0wlkons1  30191  trlsegvdeg  30297  fsumiunle  32902  cycpmco2lem1  33187  cycpmco2lem5  33191  cycpmco2  33194  cycpmconjv  33203  cyc3conja  33218  idomsubr  33370  islbs5  33440  extdgfialglem1  33836  qqhre  34164  esumiun  34238  erdszelem4  35376  erdszelem8  35380  erdszelem9  35381  erdsze2lem2  35386  mh-inf3f1  36723  pibt2  37733  aks6d1c2  42569  aks6d1c6lem3  42611  diophrw  43191  eldioph2lem2  43193  eldioph2  43194  eldioph2b  43195  dnwech  43476  cantnfub2  43750  seff  44736  fargshiftf1  47901  fmtnoinf  47999  upgrimtrlslem2  48381  ushggricedg  48403  grtrimap  48424  oppff1o  49624  fucoppcid  49883  diag1f1o  50009  diag2f1o  50012