Theorem dff1o3 6834

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 6833	. 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 1570  ^◡ccnv 5665  ran crn 5667  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 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2156  ax-ext 2738

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

This theorem is used by:  f1ofo  6835  resdif  6849  f1opw  7679  f11o  7953  1stconst  8104  2ndconst  8105  curry1  8108  curry2  8111  f1o2ndf1  8126  ssdomg  9006  dif1enlem  9154  phplem2  9199  php3  9203  f1opwfi  9323  cantnfp1lem3  9659  fpwwe2lem5  10638  canthp1lem2  10656  odf1o2  19668  dprdf1o  20129  relogf1o  26761  iseupthf1o  30583  padct  33093  ballotlemfrc  34941  poimirlem1  38305  poimirlem2  38306  poimirlem3  38307  poimirlem4  38308  poimirlem6  38310  poimirlem7  38311  poimirlem9  38313  poimirlem11  38315  poimirlem12  38316  poimirlem13  38317  poimirlem14  38318  poimirlem16  38320  poimirlem17  38321  poimirlem19  38323  poimirlem20  38324  poimirlem23  38327  poimirlem24  38328  poimirlem25  38329  poimirlem29  38333  poimirlem31  38335  ntrneifv2  44839  permaxpow  45751  upgrimpthslem1  48705  upgrimspths  48708  idfth  49969  idsubc  49971