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

Theorem dff1o3 6388
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 1122 . 2 ((𝐹 Fn 𝐴 ∧ Fun 𝐹 ∧ ran 𝐹 = 𝐵) ↔ ((𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵) ∧ Fun 𝐹))
2 dff1o2 6387 . 2 (𝐹:𝐴1-1-onto𝐵 ↔ (𝐹 Fn 𝐴 ∧ Fun 𝐹 ∧ ran 𝐹 = 𝐵))
3 df-fo 6133 . . 3 (𝐹:𝐴onto𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵))
43anbi1i 617 . 2 ((𝐹:𝐴onto𝐵 ∧ Fun 𝐹) ↔ ((𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵) ∧ Fun 𝐹))
51, 2, 43bitr4i 295 1 (𝐹:𝐴1-1-onto𝐵 ↔ (𝐹:𝐴onto𝐵 ∧ Fun 𝐹))
Colors of variables: wff setvar class
Syntax hints:  wb 198  wa 386  w3a 1111   = wceq 1656  ccnv 5345  ran crn 5347  Fun wfun 6121   Fn wfn 6122  ontowfo 6125  1-1-ontowf1o 6126
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009  ax-6 2075  ax-7 2112  ax-9 2173  ax-10 2192  ax-11 2207  ax-12 2220  ax-ext 2803
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 879  df-3an 1113  df-tru 1660  df-ex 1879  df-nf 1883  df-sb 2068  df-clab 2812  df-cleq 2818  df-clel 2821  df-in 3805  df-ss 3812  df-f 6131  df-f1 6132  df-fo 6133  df-f1o 6134
This theorem is referenced by:  f1ofo  6389  resdif  6402  f1opw  7154  f11o  7395  1stconst  7534  2ndconst  7535  curry1  7538  curry2  7541  f1o2ndf1  7554  ssdomg  8274  phplem4  8417  php3  8421  f1opwfi  8545  cantnfp1lem3  8861  fpwwe2lem6  9779  canthp1lem2  9797  odf1o2  18346  dprdf1o  18792  relogf1o  24719  iseupthf1o  27574  padct  30041  ballotlemfrc  31130  poimirlem1  33953  poimirlem2  33954  poimirlem3  33955  poimirlem4  33956  poimirlem6  33958  poimirlem7  33959  poimirlem9  33961  poimirlem11  33963  poimirlem12  33964  poimirlem13  33965  poimirlem14  33966  poimirlem16  33968  poimirlem17  33969  poimirlem19  33971  poimirlem20  33972  poimirlem23  33975  poimirlem24  33976  poimirlem25  33977  poimirlem29  33981  poimirlem31  33983  ntrneifv2  39217
  Copyright terms: Public domain W3C validator