Theorem dff1o3 6853

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 6852	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ Fun ◡𝐹 ∧ ran 𝐹 = 𝐵))
3		df-fo 6566	. . 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 1539  ^◡ccnv 5683  ran crn 5685  Fun wfun 6554   Fn wfn 6555  –onto→wfo 6558  –1-1-onto→wf1o 6559

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-9 2117  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-ex 1779  df-cleq 2728  df-ss 3967  df-f 6564  df-f1 6565  df-fo 6566  df-f1o 6567

This theorem is referenced by:  f1ofo  6854  resdif  6868  f1opw  7690  f11o  7972  1stconst  8126  2ndconst  8127  curry1  8130  curry2  8133  f1o2ndf1  8148  ssdomg  9041  dif1enlem  9197  dif1enlemOLD  9198  phplem2  9246  php3  9250  phplem4OLD  9258  php3OLD  9262  f1opwfi  9397  cantnfp1lem3  9721  fpwwe2lem5  10676  canthp1lem2  10694  odf1o2  19592  dprdf1o  20053  relogf1o  26609  iseupthf1o  30222  padct  32732  ballotlemfrc  34530  poimirlem1  37629  poimirlem2  37630  poimirlem3  37631  poimirlem4  37632  poimirlem6  37634  poimirlem7  37635  poimirlem9  37637  poimirlem11  37639  poimirlem12  37640  poimirlem13  37641  poimirlem14  37642  poimirlem16  37644  poimirlem17  37645  poimirlem19  37647  poimirlem20  37648  poimirlem23  37651  poimirlem24  37652  poimirlem25  37653  poimirlem29  37657  poimirlem31  37659  ntrneifv2  44098