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

Theorem f1eq2 5449
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 5392 . . 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 5276 . 2  |-  ( F : A -1-1-> C  <->  ( F : A --> C  /\  Fun  `' F ) )
4 df-f1 5276 . 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 1632   `'ccnv 4704   Fun wfun 5265   -->wf 5267   -1-1->wf1 5268
This theorem is referenced by:  f1oeq2  5480  f1eq123d  5483  brdomg  6888  marypha1lem  7202  fseqenlem1  7667  dfac12lem2  7786  dfac12lem3  7787  ackbij2  7885  iundom2g  8178  hashf1  11411  eldioph2lem2  26943  isuslgra  28234  isusgra  28235  usgra0  28250  uslgra1  28252  usgra1  28253  fargshiftf1  28382  usgrcyclnl2  28387  4cycl4dv  28413
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-11 1727  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-an 360  df-cleq 2289  df-fn 5274  df-f 5275  df-f1 5276
  Copyright terms: Public domain W3C validator