Theorem dff1o3 6836

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 1113	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ Fun ◡𝐹 ∧ ran 𝐹 = 𝐵) ↔ ((𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵) ∧ Fun ◡𝐹))
2		dff1o2 6835	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ Fun ◡𝐹 ∧ ran 𝐹 = 𝐵))
3		df-fo 6549	. . 3 ⊢ (𝐹:𝐴–onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵))
4	3	anbi1i 636	. 2 ⊢ ((𝐹:𝐴–onto→𝐵 ∧ Fun ◡𝐹) ↔ ((𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵) ∧ Fun ◡𝐹))
5	1, 2, 4	3bitr4i 306	1 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹:𝐴–onto→𝐵 ∧ Fun ◡𝐹))

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401   ∧ w3a 1103   = wceq 1569  ^◡ccnv 5650  ran crn 5652  Fun wfun 6537   Fn wfn 6538  –onto→wfo 6541  –1-1-onto→wf1o 6542

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105  df-ex 1812  df-cleq 2752  df-ss 3897  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550

This theorem is used by:  f1ofo  6837  resdif  6851  f1opw  7681  f11o  7963  1stconst  8117  2ndconst  8118  curry1  8121  curry2  8124  f1o2ndf1  8139  ssdomg  9034  dif1enlem  9182  phplem2  9227  php3  9231  f1opwfi  9352  cantnfp1lem3  9688  fpwwe2lem5  10727  canthp1lem2  10745  odf1o2  19796  dprdf1o  20257  relogf1o  26903  iseupthf1o  30812  padct  33361  ballotlemfrc  35209  poimirlem1  38648  poimirlem2  38649  poimirlem3  38650  poimirlem4  38651  poimirlem6  38653  poimirlem7  38654  poimirlem9  38656  poimirlem11  38658  poimirlem12  38659  poimirlem13  38660  poimirlem14  38661  poimirlem16  38663  poimirlem17  38664  poimirlem19  38666  poimirlem20  38667  poimirlem23  38670  poimirlem24  38671  poimirlem25  38672  poimirlem29  38676  poimirlem31  38678  ntrneifv2  45189  permaxpow  46107  hfstructhf  46138  upgrimpthslem1  49113  upgrimspths  49116  idfth  50382  idsubc  50384