Theorem dff1o3 6777

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 6776	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ Fun ◡𝐹 ∧ ran 𝐹 = 𝐵))
3		df-fo 6495	. . 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 5620  ran crn 5622  Fun wfun 6483   Fn wfn 6484  –onto→wfo 6487  –1-1-onto→wf1o 6488

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 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-ex 1781  df-cleq 2725  df-ss 3915  df-f 6493  df-f1 6494  df-fo 6495  df-f1o 6496

This theorem is referenced by:  f1ofo  6778  resdif  6792  f1opw  7611  f11o  7888  1stconst  8039  2ndconst  8040  curry1  8043  curry2  8046  f1o2ndf1  8061  ssdomg  8933  dif1enlem  9080  phplem2  9125  php3  9129  f1opwfi  9251  cantnfp1lem3  9581  fpwwe2lem5  10537  canthp1lem2  10555  odf1o2  19493  dprdf1o  19954  relogf1o  26522  iseupthf1o  30203  padct  32725  ballotlemfrc  34612  poimirlem1  37734  poimirlem2  37735  poimirlem3  37736  poimirlem4  37737  poimirlem6  37739  poimirlem7  37740  poimirlem9  37742  poimirlem11  37744  poimirlem12  37745  poimirlem13  37746  poimirlem14  37747  poimirlem16  37749  poimirlem17  37750  poimirlem19  37752  poimirlem20  37753  poimirlem23  37756  poimirlem24  37757  poimirlem25  37758  poimirlem29  37762  poimirlem31  37764  ntrneifv2  44237  permaxpow  45166  upgrimpthslem1  48069  upgrimspths  48072  idfth  49319  idsubc  49321