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

Theorem f1eq2 5782
Description: Equality theorem for one-to-one functions. (Contributed by NM, 10-Feb-1997.)
Assertion
Ref Expression
f1eq2

Proof of Theorem f1eq2
StepHypRef Expression
1 feq2 5719 . . 3
21anbi1d 704 . 2
3 df-f1 5598 . 2
4 df-f1 5598 . 2
52, 3, 43bitr4g 288 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  /\wa 369  =wceq 1395  `'ccnv 5003  Funwfun 5587  -->wf 5589  -1-1->wf1 5590
This theorem is referenced by:  f1oeq2  5813  f1eq123d  5816  brdomg  7546  marypha1lem  7913  fseqenlem1  8426  dfac12lem2  8545  dfac12lem3  8546  ackbij2  8644  iundom2g  8936  hashf1  12506  isuslgra  24343  isusgra  24344  ausisusgra  24355  usgra0  24370  uslgra1  24372  usgra1  24373  cusgraexilem2  24467  2trllemE  24555  constr1trl  24590  fargshiftf1  24637  usgrcyclnl2  24641  4cycl4dv  24667  eldioph2lem2  30694  usgra2pthlem1  32353  usgra2pth  32354  aacllem  33216
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-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-cleq 2449  df-fn 5596  df-f 5597  df-f1 5598
  Copyright terms: Public domain W3C validator