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

Theorem dff1o3 5758
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 977 . 2  |-  ( ( F  Fn  A  /\  Fun  `' F  /\  ran  F  =  B )  <->  ( ( F  Fn  A  /\  ran  F  =  B )  /\  Fun  `' F
) )
2 dff1o2 5757 . 2  |-  ( F : A -1-1-onto-> B  <->  ( F  Fn  A  /\  Fun  `' F  /\  ran  F  =  B ) )
3 df-fo 5535 . . 3  |-  ( F : A -onto-> B  <->  ( F  Fn  A  /\  ran  F  =  B ) )
43anbi1i 695 . 2  |-  ( ( F : A -onto-> B  /\  Fun  `' F )  <-> 
( ( F  Fn  A  /\  ran  F  =  B )  /\  Fun  `' F ) )
51, 2, 43bitr4i 277 1  |-  ( F : A -1-1-onto-> B  <->  ( F : A -onto-> B  /\  Fun  `' F ) )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    /\ wa 369    /\ w3a 965    = wceq 1370   `'ccnv 4950   ran crn 4952   Fun wfun 5523    Fn wfn 5524   -onto->wfo 5527   -1-1-onto->wf1o 5528
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-in 3446  df-ss 3453  df-f 5533  df-f1 5534  df-fo 5535  df-f1o 5536
This theorem is referenced by:  f1ofo  5759  resdif  5772  f1opw  6427  f11o  6652  1stconst  6774  2ndconst  6775  curry1  6777  curry2  6780  f1o2ndf1  6793  ssdomg  7468  phplem4  7606  php3  7610  f1opwfi  7729  cantnfp1lem3  8002  cantnfp1lem3OLD  8028  mapfienOLD  8041  fpwwe2lem6  8916  canthp1lem2  8934  odf1o2  16196  dprdf1o  16654  relogf1o  22154  ballotlemfrc  27073
  Copyright terms: Public domain W3C validator