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

Theorem dff1o4 5729
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 5726 . 2
2 3anass 941 . 2
3 df-rn 4930 . . . . . 6
43eqeq1i 2450 . . . . 5
54anbi2i 677 . . . 4
6 df-fn 5504 . . . 4
75, 6bitr4i 245 . . 3
87anbi2i 677 . 2
91, 2, 83bitri 264 1
Colors of variables: wff set class
Syntax hints:  <->wb 178  /\wa 360  /\w3a 937  =wceq 1654  `'ccnv 4918  domcdm 4919  rancrn 4920  Funwfun 5495  Fnwfn 5496  -1-1-onto->wf1o 5500
This theorem is referenced by:  f1ocnv  5734  f1oun  5741  f1o00  5757  f1oi  5760  f1osn  5762  f1oprswap  5764  f1ompt  5939  f1ocnvd  6343  curry1  6488  curry2  6491  f1ofveu  6633  mapsnf1o2  7110  omxpenlem  7258  sbthlem9  7274  compssiso  8305  fsumrev  12613  fsumshft  12614  invf1o  14045  grpinvf1o  14912  ghmf1o  15086  srngf1o  15993  lmhmf1o  16173  hmeof1o2  17846  f1o3d  24089  f1od2  24718  fprodshft  25404  fprodrev  25405  axcontlem2  26008  cdleme51finvN  31593
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1628  ax-9 1669  ax-8 1690  ax-6 1747  ax-7 1752  ax-11 1764  ax-12 1954  ax-ext 2424
This theorem depends on definitions:  df-bi 179  df-an 362  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1661  df-clab 2430  df-cleq 2436  df-clel 2439  df-in 3316  df-ss 3323  df-rn 4930  df-fn 5504  df-f 5505  df-f1 5506  df-fo 5507  df-f1o 5508
  Copyright terms: Public domain W3C validator