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

Theorem dff1o3 5494
Description: Alternate definition of one-to-one onto function. (Contributed by NM, 25-Mar-1998.) (Proof shortened by Andrew Salmon, 22-Oct-2011.)
Assertion
Ref Expression
dff1o3  |-  ( F : A -1-1-onto-> B  <->  ( F : A -onto-> B  /\  Fun  `' F ) )

Proof of Theorem dff1o3
StepHypRef Expression
1 3anan32 946 . 2  |-  ( ( F  Fn  A  /\  Fun  `' F  /\  ran  F  =  B )  <->  ( ( F  Fn  A  /\  ran  F  =  B )  /\  Fun  `' F
) )
2 dff1o2 5493 . 2  |-  ( F : A -1-1-onto-> B  <->  ( F  Fn  A  /\  Fun  `' F  /\  ran  F  =  B ) )
3 df-fo 5277 . . 3  |-  ( F : A -onto-> B  <->  ( F  Fn  A  /\  ran  F  =  B ) )
43anbi1i 676 . 2  |-  ( ( F : A -onto-> B  /\  Fun  `' F )  <-> 
( ( F  Fn  A  /\  ran  F  =  B )  /\  Fun  `' F ) )
51, 2, 43bitr4i 268 1  |-  ( F : A -1-1-onto-> B  <->  ( F : A -onto-> B  /\  Fun  `' F ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 176    /\ wa 358    /\ w3a 934    = wceq 1632   `'ccnv 4704   ran crn 4706   Fun wfun 5265    Fn wfn 5266   -onto->wfo 5269   -1-1-onto->wf1o 5270
This theorem is referenced by:  f1ofo  5495  resdif  5510  f11o  5522  f1opw  6088  1stconst  6223  2ndconst  6224  curry1  6226  curry2  6229  ssdomg  6923  phplem4  7059  php3  7063  f1opwfi  7175  cantnfp1lem3  7398  mapfien  7415  fpwwe2lem6  8273  canthp1lem2  8291  odf1o2  14900  dprdf1o  15283  relogf1o  19940  ballotlemfrc  23101  domrancur1b  25303
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-an 360  df-3an 936  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-in 3172  df-ss 3179  df-f 5275  df-f1 5276  df-fo 5277  df-f1o 5278
  Copyright terms: Public domain W3C validator