Theorem dff1o3 6774

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 6773	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ Fun ◡𝐹 ∧ ran 𝐹 = 𝐵))
3		df-fo 6492	. . 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 5622  ran crn 5624  Fun wfun 6480   Fn wfn 6481  –onto→wfo 6484  –1-1-onto→wf1o 6485

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 3922  df-f 6490  df-f1 6491  df-fo 6492  df-f1o 6493

This theorem is referenced by:  f1ofo  6775  resdif  6789  f1opw  7609  f11o  7889  1stconst  8040  2ndconst  8041  curry1  8044  curry2  8047  f1o2ndf1  8062  ssdomg  8932  dif1enlem  9080  dif1enlemOLD  9081  phplem2  9129  php3  9133  f1opwfi  9265  cantnfp1lem3  9595  fpwwe2lem5  10548  canthp1lem2  10566  odf1o2  19470  dprdf1o  19931  relogf1o  26491  iseupthf1o  30164  padct  32676  ballotlemfrc  34497  poimirlem1  37603  poimirlem2  37604  poimirlem3  37605  poimirlem4  37606  poimirlem6  37608  poimirlem7  37609  poimirlem9  37611  poimirlem11  37613  poimirlem12  37614  poimirlem13  37615  poimirlem14  37616  poimirlem16  37618  poimirlem17  37619  poimirlem19  37621  poimirlem20  37622  poimirlem23  37625  poimirlem24  37626  poimirlem25  37627  poimirlem29  37631  poimirlem31  37633  ntrneifv2  44056  permaxpow  44986  upgrimpthslem1  47895  upgrimspths  47898  idfth  49147  idsubc  49149