Theorem dff1o3 6786

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 1097	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ Fun ◡𝐹 ∧ ran 𝐹 = 𝐵) ↔ ((𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵) ∧ Fun ◡𝐹))
2		dff1o2 6785	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ Fun ◡𝐹 ∧ ran 𝐹 = 𝐵))
3		df-fo 6504	. . 3 ⊢ (𝐹:𝐴–onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵))
4	3	anbi1i 625	. 2 ⊢ ((𝐹:𝐴–onto→𝐵 ∧ Fun ◡𝐹) ↔ ((𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵) ∧ Fun ◡𝐹))
5	1, 2, 4	3bitr4i 303	1 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹:𝐴–onto→𝐵 ∧ Fun ◡𝐹))

Syntax hints:   ↔ wb 206   ∧ wa 395   ∧ w3a 1087   = wceq 1542  ^◡ccnv 5630  ran crn 5632  Fun wfun 6492   Fn wfn 6493  –onto→wfo 6496  –1-1-onto→wf1o 6497

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 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1089  df-ex 1782  df-cleq 2728  df-ss 3906  df-f 6502  df-f1 6503  df-fo 6504  df-f1o 6505

This theorem is referenced by:  f1ofo  6787  resdif  6801  f1opw  7623  f11o  7900  1stconst  8050  2ndconst  8051  curry1  8054  curry2  8057  f1o2ndf1  8072  ssdomg  8947  dif1enlem  9094  phplem2  9139  php3  9143  f1opwfi  9266  cantnfp1lem3  9601  fpwwe2lem5  10558  canthp1lem2  10576  odf1o2  19548  dprdf1o  20009  relogf1o  26530  iseupthf1o  30272  padct  32791  ballotlemfrc  34671  poimirlem1  37942  poimirlem2  37943  poimirlem3  37944  poimirlem4  37945  poimirlem6  37947  poimirlem7  37948  poimirlem9  37950  poimirlem11  37952  poimirlem12  37953  poimirlem13  37954  poimirlem14  37955  poimirlem16  37957  poimirlem17  37958  poimirlem19  37960  poimirlem20  37961  poimirlem23  37964  poimirlem24  37965  poimirlem25  37966  poimirlem29  37970  poimirlem31  37972  ntrneifv2  44507  permaxpow  45436  upgrimpthslem1  48383  upgrimspths  48386  idfth  49633  idsubc  49635