Theorem f1f 6804

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

Syntax hints:   → wi 4  ^◡ccnv 5684  Fun wfun 6555  ⟶wf 6557  –1-1→wf1 6558

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 6566

This theorem is referenced by:  f1fn  6805  f1ss  6809  f1ssres  6811  f1co  6815  f1of  6848  dff1o5  6857  f1un  6868  fsnd  6891  f1cofveqaeq  7278  f1cofveqaeqALT  7279  2f1fvneq  7280  f1dom3el3dif  7289  f1cdmsn  7302  f1prex  7304  cocan1  7311  fvf1pr  7327  f1iun  7968  f1dmex  7981  f1o2ndf1  8147  oacomf1olem  8602  brdomg  8997  brdomgOLD  8998  f1dom2g  9010  f1domg  9012  dom3d  9034  f1imaen2g  9055  2dom  9070  domdifsn  9094  xpdom2  9107  domunsncan  9112  sucdom2OLD  9122  dom0  9142  fodomr  9168  domss2  9176  domssex2  9177  f1domfi  9221  sucdom2  9243  f1finf1o  9305  f1finf1oOLD  9306  infn0  9340  f1fi  9352  fodomfir  9368  oiexg  9575  hartogslem1  9582  infdifsn  9697  fseqenlem1  10064  fseqenlem2  10065  ac10ct  10074  acndom  10091  acndom2  10094  dfac12lem2  10185  dfac12lem3  10186  ackbij1  10277  fictb  10284  cfsmolem  10310  cfcoflem  10312  cfcof  10314  fin23lem17  10378  fin23lem32  10384  fin23lem39  10390  fin23lem41  10392  fin1a2lem6  10445  fin1a2lem7  10446  iundom2g  10580  alephreg  10622  canthnumlem  10688  canthwelem  10690  pwfseqlem1  10698  pwfseqlem5  10703  fvf1tp  13829  seqf1olem1  14082  hashf1rn  14391  hashimarn  14479  hashf1dmcdm  14483  hashf1lem1  14494  hashf1lem2  14495  cshf1  14848  setcmon  18132  injsubmefmnd  18910  odinf  19581  odcl2  19583  sylow1lem2  19617  gsumval3lem1  19923  gsumval3lem2  19924  gsumval3  19925  gsumzcl2  19928  gsumzf1o  19930  gsumzaddlem  19939  gsumzmhm  19955  gsumzoppg  19962  dprdf1  20053  f1lindf  21842  f1linds  21845  lindfmm  21847  mdetunilem8  22625  2ndcdisj  23464  itg1addlem4  25734  reeff1o  26491  birthdaylem1  26994  dchrisum0fno1  27555  ushgruhgr  29086  umgr0e  29127  usgredgss  29176  ausgrusgrb  29182  usgrss  29191  uspgrupgr  29195  usgrumgr  29198  usgruspgrb  29200  usgrislfuspgr  29204  usgredg2ALT  29210  ushgredgedg  29246  ushgredgedgloop  29248  usgr2pth  29784  0wlkons1  30140  trlsegvdeg  30246  fsumiunle  32831  cycpmco2lem1  33146  cycpmco2lem5  33150  cycpmco2  33153  cycpmconjv  33162  cyc3conja  33177  idomsubr  33311  islbs5  33408  qqhre  34021  esumiun  34095  erdszelem4  35199  erdszelem8  35203  erdszelem9  35204  erdsze2lem2  35209  pibt2  37418  aks6d1c2  42131  aks6d1c6lem3  42173  diophrw  42770  eldioph2lem2  42772  eldioph2  42773  eldioph2b  42774  dnwech  43060  cantnfub2  43335  seff  44328  fargshiftf1  47428  fmtnoinf  47523  ushggricedg  47896  grtrimap  47915