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 1096	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ Fun ◡𝐹 ∧ ran 𝐹 = 𝐵) ↔ ((𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵) ∧ Fun ◡𝐹))
2		dff1o2 6787	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ Fun ◡𝐹 ∧ ran 𝐹 = 𝐵))
3		df-fo 6505	. . 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 1540  ^◡ccnv 5630  ran crn 5632  Fun wfun 6493   Fn wfn 6494  –onto→wfo 6497  –1-1-onto→wf1o 6498

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-ex 1780  df-cleq 2721  df-ss 3928  df-f 6503  df-f1 6504  df-fo 6505  df-f1o 6506

This theorem is referenced by:  f1ofo  6789  resdif  6803  f1opw  7625  f11o  7905  1stconst  8056  2ndconst  8057  curry1  8060  curry2  8063  f1o2ndf1  8078  ssdomg  8948  dif1enlem  9097  dif1enlemOLD  9098  phplem2  9146  php3  9150  f1opwfi  9283  cantnfp1lem3  9609  fpwwe2lem5  10564  canthp1lem2  10582  odf1o2  19479  dprdf1o  19940  relogf1o  26451  iseupthf1o  30104  padct  32616  ballotlemfrc  34491  poimirlem1  37588  poimirlem2  37589  poimirlem3  37590  poimirlem4  37591  poimirlem6  37593  poimirlem7  37594  poimirlem9  37596  poimirlem11  37598  poimirlem12  37599  poimirlem13  37600  poimirlem14  37601  poimirlem16  37603  poimirlem17  37604  poimirlem19  37606  poimirlem20  37607  poimirlem23  37610  poimirlem24  37611  poimirlem25  37612  poimirlem29  37616  poimirlem31  37618  ntrneifv2  44042  permaxpow  44972  upgrimpthslem1  47880  upgrimspths  47883  idfth  49120  idsubc  49122