Theorem dff1o3 6827

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 6826	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ Fun ◡𝐹 ∧ ran 𝐹 = 𝐵))
3		df-fo 6542	. . 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 1103   = wceq 1570  ^◡ccnv 5660  ran crn 5662  Fun wfun 6530   Fn wfn 6531  –onto→wfo 6534  –1-1-onto→wf1o 6535

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-3an 1105  df-ex 1810  df-cleq 2755  df-ss 3922  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543

This theorem is referenced by:  f1ofo  6828  resdif  6842  f1opw  7666  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  10615  canthp1lem2  10633  odf1o2  19638  dprdf1o  20099  relogf1o  26731  iseupthf1o  30553  padct  33063  ballotlemfrc  34917  poimirlem1  38272  poimirlem2  38273  poimirlem3  38274  poimirlem4  38275  poimirlem6  38277  poimirlem7  38278  poimirlem9  38280  poimirlem11  38282  poimirlem12  38283  poimirlem13  38284  poimirlem14  38285  poimirlem16  38287  poimirlem17  38288  poimirlem19  38290  poimirlem20  38291  poimirlem23  38294  poimirlem24  38295  poimirlem25  38296  poimirlem29  38300  poimirlem31  38302  ntrneifv2  44806  permaxpow  45718  upgrimpthslem1  48672  upgrimspths  48675  idfth  49936  idsubc  49938