Theorem dff1o3 6868

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 6867	. 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ Fun ◡𝐹 ∧ ran 𝐹 = 𝐵))
3		df-fo 6579	. . 3 ⊢ (𝐹:𝐴–onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵))
4	3	anbi1i 623	. 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 1537  ^◡ccnv 5699  ran crn 5701  Fun wfun 6567   Fn wfn 6568  –onto→wfo 6571  –1-1-onto→wf1o 6572

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1089  df-ex 1778  df-cleq 2732  df-ss 3993  df-f 6577  df-f1 6578  df-fo 6579  df-f1o 6580

This theorem is referenced by:  f1ofo  6869  resdif  6883  f1opw  7706  f11o  7987  1stconst  8141  2ndconst  8142  curry1  8145  curry2  8148  f1o2ndf1  8163  ssdomg  9060  dif1enlem  9222  dif1enlemOLD  9223  phplem2  9271  php3  9275  phplem4OLD  9283  php3OLD  9287  f1opwfi  9426  cantnfp1lem3  9749  fpwwe2lem5  10704  canthp1lem2  10722  odf1o2  19615  dprdf1o  20076  relogf1o  26626  iseupthf1o  30234  padct  32733  ballotlemfrc  34491  poimirlem1  37581  poimirlem2  37582  poimirlem3  37583  poimirlem4  37584  poimirlem6  37586  poimirlem7  37587  poimirlem9  37589  poimirlem11  37591  poimirlem12  37592  poimirlem13  37593  poimirlem14  37594  poimirlem16  37596  poimirlem17  37597  poimirlem19  37599  poimirlem20  37600  poimirlem23  37603  poimirlem24  37604  poimirlem25  37605  poimirlem29  37609  poimirlem31  37611  ntrneifv2  44042