Theorem dff1o3 6596

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

Syntax hints:   ↔ wb 209   ∧ wa 399   ∧ w3a 1084   = wceq 1538  ^◡ccnv 5518  ran crn 5520  Fun wfun 6318   Fn wfn 6319  –onto→wfo 6322  –1-1-onto→wf1o 6323

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-3an 1086  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-in 3888  df-ss 3898  df-f 6328  df-f1 6329  df-fo 6330  df-f1o 6331

This theorem is referenced by:  f1ofo  6597  resdif  6610  f1opw  7381  f11o  7630  1stconst  7778  2ndconst  7779  curry1  7782  curry2  7785  f1o2ndf1  7801  ssdomg  8538  phplem4  8683  php3  8687  f1opwfi  8812  cantnfp1lem3  9127  fpwwe2lem6  10046  canthp1lem2  10064  odf1o2  18690  dprdf1o  19147  relogf1o  25158  iseupthf1o  27987  padct  30481  ballotlemfrc  31894  poimirlem1  35058  poimirlem2  35059  poimirlem3  35060  poimirlem4  35061  poimirlem6  35063  poimirlem7  35064  poimirlem9  35066  poimirlem11  35068  poimirlem12  35069  poimirlem13  35070  poimirlem14  35071  poimirlem16  35073  poimirlem17  35074  poimirlem19  35076  poimirlem20  35077  poimirlem23  35080  poimirlem24  35081  poimirlem25  35082  poimirlem29  35086  poimirlem31  35088  ntrneifv2  40783