Theorem dff1o3 6806

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 1096	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ Fun ◡𝐹 ∧ ran 𝐹 = 𝐵) ↔ ((𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵) ∧ Fun ◡𝐹))
2		dff1o2 6805	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ Fun ◡𝐹 ∧ ran 𝐹 = 𝐵))
3		df-fo 6517	. . 3 ⊢ (𝐹:𝐴–onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵))
4	3	anbi1i 624	. 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 1086   = wceq 1540  ^◡ccnv 5637  ran crn 5639  Fun wfun 6505   Fn wfn 6506  –onto→wfo 6509  –1-1-onto→wf1o 6510

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-ex 1780  df-cleq 2721  df-ss 3931  df-f 6515  df-f1 6516  df-fo 6517  df-f1o 6518

This theorem is referenced by:  f1ofo  6807  resdif  6821  f1opw  7645  f11o  7925  1stconst  8079  2ndconst  8080  curry1  8083  curry2  8086  f1o2ndf1  8101  ssdomg  8971  dif1enlem  9120  dif1enlemOLD  9121  phplem2  9169  php3  9173  f1opwfi  9307  cantnfp1lem3  9633  fpwwe2lem5  10588  canthp1lem2  10606  odf1o2  19503  dprdf1o  19964  relogf1o  26475  iseupthf1o  30131  padct  32643  ballotlemfrc  34518  poimirlem1  37615  poimirlem2  37616  poimirlem3  37617  poimirlem4  37618  poimirlem6  37620  poimirlem7  37621  poimirlem9  37623  poimirlem11  37625  poimirlem12  37626  poimirlem13  37627  poimirlem14  37628  poimirlem16  37630  poimirlem17  37631  poimirlem19  37633  poimirlem20  37634  poimirlem23  37637  poimirlem24  37638  poimirlem25  37639  poimirlem29  37643  poimirlem31  37645  ntrneifv2  44069  permaxpow  44999  upgrimpthslem1  47907  upgrimspths  47910  idfth  49147  idsubc  49149