New Foundations Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  NFE Home  >  Th. List  >  dff1o2 Unicode version

Theorem dff1o2 5291
 Description: Alternate definition of one-to-one onto function. (The proof was shortened by Andrew Salmon, 22-Oct-2011.) (Contributed by set.mm contributors, 10-Feb-1997.) (Revised by set.mm contributors, 22-Oct-2011.)
Assertion
Ref Expression
dff1o2

Proof of Theorem dff1o2
StepHypRef Expression
1 df-f1o 4794 . 2
2 df-f1 4792 . . 3
3 df-fo 4793 . . 3
42, 3anbi12i 678 . 2
5 ancom 437 . . . 4
6 3anass 938 . . . . . 6
7 an12 772 . . . . . 6
86, 7bitri 240 . . . . 5
98anbi1i 676 . . . 4
105, 9bitr4i 243 . . 3
11 anass 630 . . 3
12 eqimss 3323 . . . . . 6
13 df-f 4791 . . . . . . 7
1413biimpri 197 . . . . . 6
1512, 14sylan2 460 . . . . 5
16153adant2 974 . . . 4
1716pm4.71i 613 . . 3
1810, 11, 173bitr4i 268 . 2
191, 4, 183bitri 262 1
 Colors of variables: wff setvar class Syntax hints:   wb 176   wa 358   w3a 934   wceq 1642   wss 3257  ccnv 4771   crn 4773   wfun 4775   wfn 4776  wf 4777  wf1 4778  wfo 4779  wf1o 4780 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925  ax-ext 2334 This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-nan 1288  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2340  df-cleq 2346  df-clel 2349  df-nfc 2478  df-v 2861  df-nin 3211  df-compl 3212  df-in 3213  df-ss 3259  df-f 4791  df-f1 4792  df-fo 4793  df-f1o 4794 This theorem is referenced by:  dff1o3  5292  dff1o4  5294  f1orn  5296  fundmen  6043  enmap1  6074  enprmap  6082  sbthlem3  6205
 Copyright terms: Public domain W3C validator