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

Theorem f1eq2 5433
Description: Equality theorem for one-to-one functions. (Contributed by NM, 10-Feb-1997.)
Assertion
Ref Expression
f1eq2  |-  ( A  =  B  ->  ( F : A -1-1-> C  <->  F : B -1-1-> C ) )

Proof of Theorem f1eq2
StepHypRef Expression
1 feq2 5376 . . 3  |-  ( A  =  B  ->  ( F : A --> C  <->  F : B
--> C ) )
21anbi1d 685 . 2  |-  ( A  =  B  ->  (
( F : A --> C  /\  Fun  `' F
)  <->  ( F : B
--> C  /\  Fun  `' F ) ) )
3 df-f1 5260 . 2  |-  ( F : A -1-1-> C  <->  ( F : A --> C  /\  Fun  `' F ) )
4 df-f1 5260 . 2  |-  ( F : B -1-1-> C  <->  ( F : B --> C  /\  Fun  `' F ) )
52, 3, 43bitr4g 279 1  |-  ( A  =  B  ->  ( F : A -1-1-> C  <->  F : B -1-1-> C ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358    = wceq 1623   `'ccnv 4688   Fun wfun 5249   -->wf 5251   -1-1->wf1 5252
This theorem is referenced by:  f1oeq2  5464  f1eq123d  5467  brdomg  6872  marypha1lem  7186  fseqenlem1  7651  dfac12lem2  7770  dfac12lem3  7771  ackbij2  7869  iundom2g  8162  hashf1  11395  eldioph2lem2  26840  isuslgra  28102  isusgra  28103  usgra0  28116  uslgra1  28118  usgra1  28119
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-11 1715  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-an 360  df-cleq 2276  df-fn 5258  df-f 5259  df-f1 5260
  Copyright terms: Public domain W3C validator