Theorem dff1o3 6770

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 6769	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ Fun ◡𝐹 ∧ ran 𝐹 = 𝐵))
3		df-fo 6488	. . 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 5618  ran crn 5620  Fun wfun 6476   Fn wfn 6477  –onto→wfo 6480  –1-1-onto→wf1o 6481

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 3920  df-f 6486  df-f1 6487  df-fo 6488  df-f1o 6489

This theorem is referenced by:  f1ofo  6771  resdif  6785  f1opw  7605  f11o  7882  1stconst  8033  2ndconst  8034  curry1  8037  curry2  8040  f1o2ndf1  8055  ssdomg  8925  dif1enlem  9073  phplem2  9119  php3  9123  f1opwfi  9246  cantnfp1lem3  9576  fpwwe2lem5  10529  canthp1lem2  10547  odf1o2  19452  dprdf1o  19913  relogf1o  26473  iseupthf1o  30146  padct  32662  ballotlemfrc  34495  poimirlem1  37601  poimirlem2  37602  poimirlem3  37603  poimirlem4  37604  poimirlem6  37606  poimirlem7  37607  poimirlem9  37609  poimirlem11  37611  poimirlem12  37612  poimirlem13  37613  poimirlem14  37614  poimirlem16  37616  poimirlem17  37617  poimirlem19  37619  poimirlem20  37620  poimirlem23  37623  poimirlem24  37624  poimirlem25  37625  poimirlem29  37629  poimirlem31  37631  ntrneifv2  44053  permaxpow  44983  upgrimpthslem1  47891  upgrimspths  47894  idfth  49143  idsubc  49145