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

Step	Hyp	Ref	Expression
1		df-f1o 5508	. 2
2		f1f 5686	. . . . 5
3	2	biantrurd 496	. . . 4
4		dffo2 5704	. . . 4
5	3, 4	syl6rbbr 257	. . 3
6	5	pm5.32i 620	. 2
7	1, 6	bitri 242	1

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