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

Theorem f1eq2 5776
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 5713 . . 3  |-  ( A  =  B  ->  ( F : A --> C  <->  F : B
--> C ) )
21anbi1d 704 . 2  |-  ( A  =  B  ->  (
( F : A --> C  /\  Fun  `' F
)  <->  ( F : B
--> C  /\  Fun  `' F ) ) )
3 df-f1 5592 . 2  |-  ( F : A -1-1-> C  <->  ( F : A --> C  /\  Fun  `' F ) )
4 df-f1 5592 . 2  |-  ( F : B -1-1-> C  <->  ( F : B --> C  /\  Fun  `' F ) )
52, 3, 43bitr4g 288 1  |-  ( A  =  B  ->  ( F : A -1-1-> C  <->  F : B -1-1-> C ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369    = wceq 1379   `'ccnv 4998   Fun wfun 5581   -->wf 5583   -1-1->wf1 5584
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-cleq 2459  df-fn 5590  df-f 5591  df-f1 5592
This theorem is referenced by:  f1oeq2  5807  f1eq123d  5810  brdomg  7526  marypha1lem  7892  fseqenlem1  8404  dfac12lem2  8523  dfac12lem3  8524  ackbij2  8622  iundom2g  8914  hashf1  12471  isuslgra  24035  isusgra  24036  ausisusgra  24047  usgra0  24062  uslgra1  24064  usgra1  24065  cusgraexilem2  24159  2trllemE  24247  constr1trl  24282  fargshiftf1  24329  usgrcyclnl2  24333  4cycl4dv  24359  eldioph2lem2  30314  usgra2pthlem1  31836  usgra2pth  31837
  Copyright terms: Public domain W3C validator