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

Theorem dff1o5 5730
Description: Alternate definition of one-to-one onto function. (Contributed by NM, 10-Dec-2003.) (Proof shortened by Andrew Salmon, 22-Oct-2011.)
Assertion
Ref Expression
dff1o5

Proof of Theorem dff1o5
StepHypRef Expression
1 df-f1o 5508 . 2
2 f1f 5686 . . . . 5
32biantrurd 496 . . . 4
4 dffo2 5704 . . . 4
53, 4syl6rbbr 257 . . 3
65pm5.32i 620 . 2
71, 6bitri 242 1
Colors of variables: wff set class
Syntax hints:  <->wb 178  /\wa 360  =wceq 1654  rancrn 4920  -->wf 5497  -1-1->wf1 5498  -onto->wfo 5499  -1-1-onto->wf1o 5500
This theorem is referenced by:  f1orescnv  5737  domdifsn  7240  sucdom2  7352  ackbij1  8169  ackbij2  8174  fin4en1  8240  om2uzf1oi  11344  s4f1o  11916  ausisusgra  21431  pwssplit4  27347  indlcim  27466  cdleme50f1o  31583  diaf1oN  32168
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1628  ax-9 1669  ax-8 1690  ax-6 1747  ax-7 1752  ax-11 1764  ax-12 1954  ax-ext 2424
This theorem depends on definitions:  df-bi 179  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1661  df-clab 2430  df-cleq 2436  df-clel 2439  df-in 3316  df-ss 3323  df-f 5505  df-f1 5506  df-fo 5507  df-f1o 5508
  Copyright terms: Public domain W3C validator