Theorem dff1o3 6764

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 1096	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ Fun ◡𝐹 ∧ ran 𝐹 = 𝐵) ↔ ((𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵) ∧ Fun ◡𝐹))
2		dff1o2 6763	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ Fun ◡𝐹 ∧ ran 𝐹 = 𝐵))
3		df-fo 6482	. . 3 ⊢ (𝐹:𝐴–onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵))
4	3	anbi1i 624	. 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 1086   = wceq 1541  ^◡ccnv 5610  ran crn 5612  Fun wfun 6470   Fn wfn 6471  –onto→wfo 6474  –1-1-onto→wf1o 6475

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-ex 1781  df-cleq 2723  df-ss 3914  df-f 6480  df-f1 6481  df-fo 6482  df-f1o 6483

This theorem is referenced by:  f1ofo  6765  resdif  6779  f1opw  7597  f11o  7874  1stconst  8025  2ndconst  8026  curry1  8029  curry2  8032  f1o2ndf1  8047  ssdomg  8917  dif1enlem  9064  phplem2  9109  php3  9113  f1opwfi  9235  cantnfp1lem3  9565  fpwwe2lem5  10521  canthp1lem2  10539  odf1o2  19480  dprdf1o  19941  relogf1o  26497  iseupthf1o  30174  padct  32693  ballotlemfrc  34532  poimirlem1  37661  poimirlem2  37662  poimirlem3  37663  poimirlem4  37664  poimirlem6  37666  poimirlem7  37667  poimirlem9  37669  poimirlem11  37671  poimirlem12  37672  poimirlem13  37673  poimirlem14  37674  poimirlem16  37676  poimirlem17  37677  poimirlem19  37679  poimirlem20  37680  poimirlem23  37683  poimirlem24  37684  poimirlem25  37685  poimirlem29  37689  poimirlem31  37691  ntrneifv2  44113  permaxpow  45042  upgrimpthslem1  47938  upgrimspths  47941  idfth  49190  idsubc  49192