Theorem dff1o3 6624

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 1098	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ Fun ◡𝐹 ∧ ran 𝐹 = 𝐵) ↔ ((𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵) ∧ Fun ◡𝐹))
2		dff1o2 6623	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ Fun ◡𝐹 ∧ ran 𝐹 = 𝐵))
3		df-fo 6345	. . 3 ⊢ (𝐹:𝐴–onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵))
4	3	anbi1i 627	. 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 1088   = wceq 1542  ^◡ccnv 5524  ran crn 5526  Fun wfun 6333   Fn wfn 6334  –onto→wfo 6337  –1-1-onto→wf1o 6338

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-ext 2710

This theorem depends on definitions:  df-bi 210  df-an 400  df-3an 1090  df-tru 1545  df-ex 1787  df-sb 2075  df-clab 2717  df-cleq 2730  df-clel 2811  df-v 3400  df-in 3850  df-ss 3860  df-f 6343  df-f1 6344  df-fo 6345  df-f1o 6346

This theorem is referenced by:  f1ofo  6625  resdif  6638  f1opw  7417  f11o  7673  1stconst  7821  2ndconst  7822  curry1  7825  curry2  7828  f1o2ndf1  7844  ssdomg  8601  phplem4  8749  php3  8753  dif1enlem  8759  f1opwfi  8901  cantnfp1lem3  9216  fpwwe2lem5  10135  canthp1lem2  10153  odf1o2  18816  dprdf1o  19273  relogf1o  25310  iseupthf1o  28139  padct  30629  ballotlemfrc  32063  poimirlem1  35401  poimirlem2  35402  poimirlem3  35403  poimirlem4  35404  poimirlem6  35406  poimirlem7  35407  poimirlem9  35409  poimirlem11  35411  poimirlem12  35412  poimirlem13  35413  poimirlem14  35414  poimirlem16  35416  poimirlem17  35417  poimirlem19  35419  poimirlem20  35420  poimirlem23  35423  poimirlem24  35424  poimirlem25  35425  poimirlem29  35429  poimirlem31  35431  ntrneifv2  41236