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

Theorem dff1o3 5828
 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

Proof of Theorem dff1o3
StepHypRef Expression
1 3anan32 985 . 2
2 dff1o2 5827 . 2
3 df-fo 5600 . . 3
43anbi1i 695 . 2
51, 2, 43bitr4i 277 1
 Colors of variables: wff setvar class Syntax hints:   wb 184   wa 369   w3a 973   wceq 1379  ccnv 5004   crn 5006   wfun 5588   wfn 5589  wfo 5592  wf1o 5593 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445 This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-in 3488  df-ss 3495  df-f 5598  df-f1 5599  df-fo 5600  df-f1o 5601 This theorem is referenced by:  f1ofo  5829  resdif  5842  f1opw  6524  f11o  6757  1stconst  6883  2ndconst  6884  curry1  6887  curry2  6890  f1o2ndf1  6903  ssdomg  7573  phplem4  7711  php3  7715  f1opwfi  7836  cantnfp1lem3  8111  cantnfp1lem3OLD  8137  mapfienOLD  8150  fpwwe2lem6  9025  canthp1lem2  9043  odf1o2  16466  dprdf1o  16951  relogf1o  22820  ballotlemfrc  28290
 Copyright terms: Public domain W3C validator