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

Theorem f1eq2 5637
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 5579 . . 3  |-  ( A  =  B  ->  ( F : A --> C  <->  F : B
--> C ) )
21anbi1d 687 . 2  |-  ( A  =  B  ->  (
( F : A --> C  /\  Fun  `' F
)  <->  ( F : B
--> C  /\  Fun  `' F ) ) )
3 df-f1 5461 . 2  |-  ( F : A -1-1-> C  <->  ( F : A --> C  /\  Fun  `' F ) )
4 df-f1 5461 . 2  |-  ( F : B -1-1-> C  <->  ( F : B --> C  /\  Fun  `' F ) )
52, 3, 43bitr4g 281 1  |-  ( A  =  B  ->  ( F : A -1-1-> C  <->  F : B -1-1-> C ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 178    /\ wa 360    = wceq 1653   `'ccnv 4879   Fun wfun 5450   -->wf 5452   -1-1->wf1 5453
This theorem is referenced by:  f1oeq2  5668  f1eq123d  5671  brdomg  7120  marypha1lem  7440  fseqenlem1  7907  dfac12lem2  8026  dfac12lem3  8027  ackbij2  8125  iundom2g  8417  hashf1  11708  isuslgra  21374  isusgra  21375  ausisusgra  21382  usgra0  21392  uslgra1  21394  usgra1  21395  cusgraexilem2  21478  2trllemE  21555  constr1trl  21590  fargshiftf1  21626  usgrcyclnl2  21630  4cycl4dv  21656  eldioph2lem2  26821  usgra2pthlem1  28312  usgra2pth  28313
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-11 1762  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-an 362  df-ex 1552  df-cleq 2431  df-fn 5459  df-f 5460  df-f1 5461
  Copyright terms: Public domain W3C validator