Theorem dff1o3 6773

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 1102	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ Fun ◡𝐹 ∧ ran 𝐹 = 𝐵) ↔ ((𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵) ∧ Fun ◡𝐹))
2		dff1o2 6772	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ Fun ◡𝐹 ∧ ran 𝐹 = 𝐵))
3		df-fo 6491	. . 3 ⊢ (𝐹:𝐴–onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵))
4	3	anbi1i 630	. 2 ⊢ ((𝐹:𝐴–onto→𝐵 ∧ Fun ◡𝐹) ↔ ((𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵) ∧ Fun ◡𝐹))
5	1, 2, 4	3bitr4i 304	1 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹:𝐴–onto→𝐵 ∧ Fun ◡𝐹))

Syntax hints:   ↔ wb 207   ∧ wa 396   ∧ w3a 1092   = wceq 1547  ^◡ccnv 5617  ran crn 5619  Fun wfun 6479   Fn wfn 6480  –onto→wfo 6483  –1-1-onto→wf1o 6484

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-3an 1094  df-ex 1787  df-cleq 2731  df-ss 3900  df-f 6489  df-f1 6490  df-fo 6491  df-f1o 6492

This theorem is referenced by:  f1ofo  6774  resdif  6788  f1opw  7612  f11o  7889  1stconst  8039  2ndconst  8040  curry1  8043  curry2  8046  f1o2ndf1  8061  ssdomg  8937  dif1enlem  9084  phplem2  9129  php3  9133  f1opwfi  9256  cantnfp1lem3  9592  fpwwe2lem5  10549  canthp1lem2  10567  odf1o2  19539  dprdf1o  20000  relogf1o  26548  iseupthf1o  30290  padct  32810  ballotlemfrc  34711  poimirlem1  37988  poimirlem2  37989  poimirlem3  37990  poimirlem4  37991  poimirlem6  37993  poimirlem7  37994  poimirlem9  37996  poimirlem11  37998  poimirlem12  37999  poimirlem13  38000  poimirlem14  38001  poimirlem16  38003  poimirlem17  38004  poimirlem19  38006  poimirlem20  38007  poimirlem23  38010  poimirlem24  38011  poimirlem25  38012  poimirlem29  38016  poimirlem31  38018  ntrneifv2  44524  permaxpow  45453  upgrimpthslem1  48398  upgrimspths  48401  idfth  49648  idsubc  49650