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

Theorem dff1o3 6830
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 1094 . 2 ((𝐹 Fn 𝐴 ∧ Fun 𝐹 ∧ ran 𝐹 = 𝐵) ↔ ((𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵) ∧ Fun 𝐹))
2 dff1o2 6829 . 2 (𝐹:𝐴1-1-onto𝐵 ↔ (𝐹 Fn 𝐴 ∧ Fun 𝐹 ∧ ran 𝐹 = 𝐵))
3 df-fo 6540 . . 3 (𝐹:𝐴onto𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 = 𝐵))
43anbi1i 623 . 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 205  wa 395  w3a 1084   = wceq 1533  ccnv 5666  ran crn 5668  Fun wfun 6528   Fn wfn 6529  ontowfo 6532  1-1-ontowf1o 6533
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2695
This theorem depends on definitions:  df-bi 206  df-an 396  df-3an 1086  df-tru 1536  df-ex 1774  df-sb 2060  df-clab 2702  df-cleq 2716  df-clel 2802  df-v 3468  df-in 3948  df-ss 3958  df-f 6538  df-f1 6539  df-fo 6540  df-f1o 6541
This theorem is referenced by:  f1ofo  6831  resdif  6845  f1opw  7656  f11o  7927  1stconst  8081  2ndconst  8082  curry1  8085  curry2  8088  f1o2ndf1  8103  ssdomg  8993  dif1enlem  9153  dif1enlemOLD  9154  phplem2  9205  php3  9209  phplem4OLD  9217  php3OLD  9221  f1opwfi  9353  cantnfp1lem3  9672  fpwwe2lem5  10627  canthp1lem2  10645  odf1o2  19485  dprdf1o  19946  relogf1o  26419  iseupthf1o  29927  padct  32416  ballotlemfrc  34017  poimirlem1  36983  poimirlem2  36984  poimirlem3  36985  poimirlem4  36986  poimirlem6  36988  poimirlem7  36989  poimirlem9  36991  poimirlem11  36993  poimirlem12  36994  poimirlem13  36995  poimirlem14  36996  poimirlem16  36998  poimirlem17  36999  poimirlem19  37001  poimirlem20  37002  poimirlem23  37005  poimirlem24  37006  poimirlem25  37007  poimirlem29  37011  poimirlem31  37013  ntrneifv2  43345
  Copyright terms: Public domain W3C validator