Theorem dff1o3 6825

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

Syntax hints:   ↔ wb 209   ∧ wa 400   ∧ w3a 1101   = wceq 1567  ^◡ccnv 5658  ran crn 5660  Fun wfun 6528   Fn wfn 6529  –onto→wfo 6532  –1-1-onto→wf1o 6533

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-3an 1103  df-ex 1807  df-cleq 2761  df-ss 3930  df-f 6538  df-f1 6539  df-fo 6540  df-f1o 6541

This theorem is referenced by:  f1ofo  6826  resdif  6840  f1opw  7664  f11o  7940  1stconst  8091  2ndconst  8092  curry1  8095  curry2  8098  f1o2ndf1  8113  ssdomg  8993  dif1enlem  9140  phplem2  9185  php3  9189  f1opwfi  9309  cantnfp1lem3  9645  fpwwe2lem5  10616  canthp1lem2  10634  odf1o2  19639  dprdf1o  20100  relogf1o  26693  iseupthf1o  30490  padct  33000  ballotlemfrc  34858  poimirlem1  38155  poimirlem2  38156  poimirlem3  38157  poimirlem4  38158  poimirlem6  38160  poimirlem7  38161  poimirlem9  38163  poimirlem11  38165  poimirlem12  38166  poimirlem13  38167  poimirlem14  38168  poimirlem16  38170  poimirlem17  38171  poimirlem19  38173  poimirlem20  38174  poimirlem23  38177  poimirlem24  38178  poimirlem25  38179  poimirlem29  38183  poimirlem31  38185  ntrneifv2  44693  permaxpow  45605  upgrimpthslem1  48556  upgrimspths  48559  idfth  49816  idsubc  49818