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

Theorem dff1o3 6853
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 6852 . 2 (𝐹:𝐴1-1-onto𝐵 ↔ (𝐹 Fn 𝐴 ∧ Fun 𝐹 ∧ ran 𝐹 = 𝐵))
3 df-fo 6566 . . 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 1539  ccnv 5683  ran crn 5685  Fun wfun 6554   Fn wfn 6555  ontowfo 6558  1-1-ontowf1o 6559
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-9 2117  ax-ext 2707
This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-ex 1779  df-cleq 2728  df-ss 3967  df-f 6564  df-f1 6565  df-fo 6566  df-f1o 6567
This theorem is referenced by:  f1ofo  6854  resdif  6868  f1opw  7690  f11o  7972  1stconst  8126  2ndconst  8127  curry1  8130  curry2  8133  f1o2ndf1  8148  ssdomg  9041  dif1enlem  9197  dif1enlemOLD  9198  phplem2  9246  php3  9250  phplem4OLD  9258  php3OLD  9262  f1opwfi  9397  cantnfp1lem3  9721  fpwwe2lem5  10676  canthp1lem2  10694  odf1o2  19592  dprdf1o  20053  relogf1o  26609  iseupthf1o  30222  padct  32732  ballotlemfrc  34530  poimirlem1  37629  poimirlem2  37630  poimirlem3  37631  poimirlem4  37632  poimirlem6  37634  poimirlem7  37635  poimirlem9  37637  poimirlem11  37639  poimirlem12  37640  poimirlem13  37641  poimirlem14  37642  poimirlem16  37644  poimirlem17  37645  poimirlem19  37647  poimirlem20  37648  poimirlem23  37651  poimirlem24  37652  poimirlem25  37653  poimirlem29  37657  poimirlem31  37659  ntrneifv2  44098
  Copyright terms: Public domain W3C validator