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

Theorem f1eq2 5792
 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 5729 . . 3
21anbi1d 709 . 2
3 df-f1 5606 . 2
4 df-f1 5606 . 2
52, 3, 43bitr4g 291 1
 Colors of variables: wff setvar class Syntax hints:   wi 4   wb 187   wa 370   wceq 1437  ccnv 4853   wfun 5595  wf 5597  wf1 5598 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-ext 2407 This theorem depends on definitions:  df-bi 188  df-an 372  df-cleq 2421  df-fn 5604  df-f 5605  df-f1 5606 This theorem is referenced by:  f1oeq2  5823  f1eq123d  5826  brdomg  7587  marypha1lem  7953  fseqenlem1  8453  dfac12lem2  8572  dfac12lem3  8573  ackbij2  8671  iundom2g  8963  hashf1  12615  istrkg3ld  24372  isuslgra  24916  isusgra  24917  ausisusgra  24928  usgra0  24943  uslgra1  24945  usgra1  24946  cusgraexilem2  25040  2trllemE  25128  constr1trl  25163  fargshiftf1  25210  usgrcyclnl2  25214  4cycl4dv  25240  eldioph2lem2  35311  usgra2pthlem1  38422  usgra2pth  38423  aacllem  39300
 Copyright terms: Public domain W3C validator