Theorem dff1o3 6788

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	⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹:𝐴–onto→𝐵 ∧ Fun ◡𝐹))

Proof of Theorem dff1o3

Step	Hyp	Ref	Expression
1		3anan32 1097	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ Fun ◡𝐹 ∧ ran 𝐹 = 𝐵) ↔ ((𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵) ∧ Fun ◡𝐹))
2		dff1o2 6787	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ Fun ◡𝐹 ∧ ran 𝐹 = 𝐵))
3		df-fo 6506	. . 3 ⊢ (𝐹:𝐴–onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵))
4	3	anbi1i 625	. 2 ⊢ ((𝐹:𝐴–onto→𝐵 ∧ Fun ◡𝐹) ↔ ((𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵) ∧ Fun ◡𝐹))
5	1, 2, 4	3bitr4i 303	1 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹:𝐴–onto→𝐵 ∧ Fun ◡𝐹))

Syntax hints:   ↔ wb 206   ∧ wa 395   ∧ w3a 1087   = wceq 1542  ^◡ccnv 5631  ran crn 5633  Fun wfun 6494   Fn wfn 6495  –onto→wfo 6498  –1-1-onto→wf1o 6499

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1089  df-ex 1782  df-cleq 2729  df-ss 3920  df-f 6504  df-f1 6505  df-fo 6506  df-f1o 6507

This theorem is referenced by:  f1ofo  6789  resdif  6803  f1opw  7624  f11o  7901  1stconst  8052  2ndconst  8053  curry1  8056  curry2  8059  f1o2ndf1  8074  ssdomg  8949  dif1enlem  9096  phplem2  9141  php3  9145  f1opwfi  9268  cantnfp1lem3  9601  fpwwe2lem5  10558  canthp1lem2  10576  odf1o2  19514  dprdf1o  19975  relogf1o  26543  iseupthf1o  30289  padct  32808  ballotlemfrc  34705  poimirlem1  37872  poimirlem2  37873  poimirlem3  37874  poimirlem4  37875  poimirlem6  37877  poimirlem7  37878  poimirlem9  37880  poimirlem11  37882  poimirlem12  37883  poimirlem13  37884  poimirlem14  37885  poimirlem16  37887  poimirlem17  37888  poimirlem19  37890  poimirlem20  37891  poimirlem23  37894  poimirlem24  37895  poimirlem25  37896  poimirlem29  37900  poimirlem31  37902  ntrneifv2  44436  permaxpow  45365  upgrimpthslem1  48267  upgrimspths  48270  idfth  49517  idsubc  49519