MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  dff1o3 Structured version   Visualization version   GIF version

Theorem dff1o3 6855
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
StepHypRef Expression
1 3anan32 1096 . 2 ((𝐹 Fn 𝐴 ∧ Fun 𝐹 ∧ ran 𝐹 = 𝐵) ↔ ((𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵) ∧ Fun 𝐹))
2 dff1o2 6854 . 2 (𝐹:𝐴1-1-onto𝐵 ↔ (𝐹 Fn 𝐴 ∧ Fun 𝐹 ∧ ran 𝐹 = 𝐵))
3 df-fo 6569 . . 3 (𝐹:𝐴onto𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵))
43anbi1i 624 . 2 ((𝐹:𝐴onto𝐵 ∧ Fun 𝐹) ↔ ((𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵) ∧ Fun 𝐹))
51, 2, 43bitr4i 303 1 (𝐹:𝐴1-1-onto𝐵 ↔ (𝐹:𝐴onto𝐵 ∧ Fun 𝐹))
Colors of variables: wff setvar class
Syntax hints:  wb 206  wa 395  w3a 1086   = wceq 1537  ccnv 5688  ran crn 5690  Fun wfun 6557   Fn wfn 6558  ontowfo 6561  1-1-ontowf1o 6562
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-9 2116  ax-ext 2706
This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-ex 1777  df-cleq 2727  df-ss 3980  df-f 6567  df-f1 6568  df-fo 6569  df-f1o 6570
This theorem is referenced by:  f1ofo  6856  resdif  6870  f1opw  7689  f11o  7970  1stconst  8124  2ndconst  8125  curry1  8128  curry2  8131  f1o2ndf1  8146  ssdomg  9039  dif1enlem  9195  dif1enlemOLD  9196  phplem2  9243  php3  9247  phplem4OLD  9255  php3OLD  9259  f1opwfi  9394  cantnfp1lem3  9718  fpwwe2lem5  10673  canthp1lem2  10691  odf1o2  19606  dprdf1o  20067  relogf1o  26623  iseupthf1o  30231  padct  32737  ballotlemfrc  34508  poimirlem1  37608  poimirlem2  37609  poimirlem3  37610  poimirlem4  37611  poimirlem6  37613  poimirlem7  37614  poimirlem9  37616  poimirlem11  37618  poimirlem12  37619  poimirlem13  37620  poimirlem14  37621  poimirlem16  37623  poimirlem17  37624  poimirlem19  37626  poimirlem20  37627  poimirlem23  37630  poimirlem24  37631  poimirlem25  37632  poimirlem29  37636  poimirlem31  37638  ntrneifv2  44070
  Copyright terms: Public domain W3C validator