MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  f1f Unicode version

Theorem f1f 5453
Description: A one-to-one mapping is a mapping. (Contributed by NM, 31-Dec-1996.)
Assertion
Ref Expression
f1f  |-  ( F : A -1-1-> B  ->  F : A --> B )

Proof of Theorem f1f
StepHypRef Expression
1 df-f1 5276 . 2  |-  ( F : A -1-1-> B  <->  ( F : A --> B  /\  Fun  `' F ) )
21simplbi 446 1  |-  ( F : A -1-1-> B  ->  F : A --> B )
Colors of variables: wff set class
Syntax hints:    -> wi 4   `'ccnv 4704   Fun wfun 5265   -->wf 5267   -1-1->wf1 5268
This theorem is referenced by:  f1fn  5454  f1ss  5458  f1ssres  5460  f1of  5488  dff1o5  5497  fun11iun  5509  f1dmex  5767  cocan1  5817  oacomf1olem  6578  brdomg  6888  f1dom2g  6895  f1domg  6897  dom3d  6919  f1imaen2g  6938  2dom  6949  domdifsn  6961  xpdom2  6973  domunsncan  6978  fodomr  7028  domss2  7036  domssex2  7037  sucdom2  7073  f1finf1o  7102  f1fi  7159  oiexg  7266  hartogslem1  7273  infdifsn  7373  fseqenlem1  7667  fseqenlem2  7668  ac10ct  7677  acndom  7694  acndom2  7697  dfac12lem2  7786  dfac12lem3  7787  ackbij1  7880  fictb  7887  cfsmolem  7912  cfcoflem  7914  cfcof  7916  fin23lem17  7980  fin23lem32  7986  fin23lem39  7992  fin23lem41  7994  fin1a2lem6  8047  fin1a2lem7  8048  iundom2g  8178  alephreg  8220  canthnumlem  8286  canthwelem  8288  pwfseqlem1  8296  pwfseqlem5  8301  seqf1olem1  11101  hashf1lem1  11409  hashf1lem2  11410  setcmon  13935  odinf  14892  odcl2  14894  odf1o1  14899  sylow1lem2  14926  gsumval3  15207  gsumzcl  15211  gsumzf1o  15212  gsumzaddlem  15219  gsumzmhm  15226  gsumzoppg  15232  dprdf1  15284  2ndcdisj  17198  itg1addlem4  19070  reeff1o  19839  birthdaylem1  20262  basellem3  20336  dchrisum0fno1  20676  erdszelem4  23740  erdszelem8  23744  erdszelem9  23745  erdsze2lem2  23750  injrec2  25222  injsurinj  25252  diophrw  26941  eldioph2lem2  26943  eldioph2  26944  eldioph2b  26945  dnwech  27248  f1lindf  27395  f1linds  27398  lindfmm  27400  seff  27641  usgrass  28244  uslisumgra  28246  usgra0v  28251  usgraedg2  28255  usgraedgrnv  28257  usgra1v  28260  fargshiftf1  28382  usgrcyclnl2  28387
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360  df-f1 5276
  Copyright terms: Public domain W3C validator