Theorem dff1o3 6780

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 6779	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ Fun ◡𝐹 ∧ ran 𝐹 = 𝐵))
3		df-fo 6498	. . 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 5623  ran crn 5625  Fun wfun 6486   Fn wfn 6487  –onto→wfo 6490  –1-1-onto→wf1o 6491

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-ex 1781  df-cleq 2728  df-ss 3918  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499

This theorem is referenced by:  f1ofo  6781  resdif  6795  f1opw  7614  f11o  7891  1stconst  8042  2ndconst  8043  curry1  8046  curry2  8049  f1o2ndf1  8064  ssdomg  8937  dif1enlem  9084  phplem2  9129  php3  9133  f1opwfi  9256  cantnfp1lem3  9589  fpwwe2lem5  10546  canthp1lem2  10564  odf1o2  19502  dprdf1o  19963  relogf1o  26531  iseupthf1o  30277  padct  32797  ballotlemfrc  34684  poimirlem1  37822  poimirlem2  37823  poimirlem3  37824  poimirlem4  37825  poimirlem6  37827  poimirlem7  37828  poimirlem9  37830  poimirlem11  37832  poimirlem12  37833  poimirlem13  37834  poimirlem14  37835  poimirlem16  37837  poimirlem17  37838  poimirlem19  37840  poimirlem20  37841  poimirlem23  37844  poimirlem24  37845  poimirlem25  37846  poimirlem29  37850  poimirlem31  37852  ntrneifv2  44321  permaxpow  45250  upgrimpthslem1  48153  upgrimspths  48156  idfth  49403  idsubc  49405