MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  dff1o4 Unicode version

Theorem dff1o4 5829
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
dff1o4

Proof of Theorem dff1o4
StepHypRef Expression
1 dff1o2 5826 . 2
2 3anass 977 . 2
3 df-rn 5015 . . . . . 6
43eqeq1i 2464 . . . . 5
54anbi2i 694 . . . 4
6 df-fn 5596 . . . 4
75, 6bitr4i 252 . . 3
87anbi2i 694 . 2
91, 2, 83bitri 271 1
Colors of variables: wff setvar class
Syntax hints:  <->wb 184  /\wa 369  /\w3a 973  =wceq 1395  `'ccnv 5003  domcdm 5004  rancrn 5005  Funwfun 5587  Fnwfn 5588  -1-1-onto->wf1o 5592
This theorem is referenced by:  f1ocnv  5833  f1oun  5840  f1o00  5853  f1oi  5856  f1osn  5858  f1oprswap  5860  f1ompt  6053  f1ofveu  6291  f1ocnvd  6524  curry1  6892  curry2  6895  mapsnf1o2  7486  omxpenlem  7638  sbthlem9  7655  compssiso  8775  mptfzshft  13593  fsumrev  13594  fprodrev  13781  invf1o  15163  mhmf1o  15976  grpinvf1o  16108  ghmf1o  16296  rhmf1o  17381  srngf1o  17503  lmhmf1o  17692  hmeof1o2  20264  axcontlem2  24268  f1o3d  27471  f1od2  27547  mgmhmf1o  32475  rnghmf1o  32709  cdleme51finvN  36282
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-in 3482  df-ss 3489  df-rn 5015  df-fn 5596  df-f 5597  df-f1 5598  df-fo 5599  df-f1o 5600
  Copyright terms: Public domain W3C validator