Theorem dff1o3 6143

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

Step	Hyp	Ref	Expression
1		3anan32 1050	. 2 |- ( ( F Fn A /\ Fun `' F /\ ran F = B ) <-> ( ( F Fn A /\ ran F = B ) /\ Fun `' F ) )
2		dff1o2 6142	. 2 |- ( F : A -1-1-onto-> B <-> ( F Fn A /\ Fun `' F /\ ran F = B ) )
3		df-fo 5894	. . 3 |- ( F : A -onto-> B <-> ( F Fn A /\ ran F = B ) )
4	3	anbi1i 731	. 2 |- ( ( F : A -onto-> B /\ Fun `' F ) <-> ( ( F Fn A /\ ran F = B ) /\ Fun `' F ) )
5	1, 2, 4	3bitr4i 292	1 |- ( F : A -1-1-onto-> B <-> ( F : A -onto-> B /\ Fun `' F ) )

Syntax hints:   <-> wb 196   /\ wa 384   /\ w3a 1037   = wceq 1483   `'ccnv 5113   ran crn 5115   Fun wfun 5882   Fn wfn 5883   -onto->wfo 5886   -1-1-onto->wf1o 5887

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-in 3581  df-ss 3588  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895

This theorem is referenced by:  f1ofo  6144  resdif  6157  f1opw  6889  f11o  7128  1stconst  7265  2ndconst  7266  curry1  7269  curry2  7272  f1o2ndf1  7285  ssdomg  8001  phplem4  8142  php3  8146  f1opwfi  8270  cantnfp1lem3  8577  fpwwe2lem6  9457  canthp1lem2  9475  odf1o2  17988  dprdf1o  18431  relogf1o  24313  iseupthf1o  27062  padct  29497  ballotlemfrc  30588  poimirlem1  33410  poimirlem2  33411  poimirlem3  33412  poimirlem4  33413  poimirlem6  33415  poimirlem7  33416  poimirlem9  33418  poimirlem11  33420  poimirlem12  33421  poimirlem13  33422  poimirlem14  33423  poimirlem16  33425  poimirlem17  33426  poimirlem19  33428  poimirlem20  33429  poimirlem23  33432  poimirlem24  33433  poimirlem25  33434  poimirlem29  33438  poimirlem31  33440  ntrneifv2  38378