MPE Home 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  |-  ( A  =  B  ->  ( F : A -1-1-> C  <->  F : B -1-1-> C ) )

Proof of Theorem f1eq2
StepHypRef Expression
1 feq2 5729 . . 3  |-  ( A  =  B  ->  ( F : A --> C  <->  F : B
--> C ) )
21anbi1d 709 . 2  |-  ( A  =  B  ->  (
( F : A --> C  /\  Fun  `' F
)  <->  ( F : B
--> C  /\  Fun  `' F ) ) )
3 df-f1 5606 . 2  |-  ( F : A -1-1-> C  <->  ( F : A --> C  /\  Fun  `' F ) )
4 df-f1 5606 . 2  |-  ( F : B -1-1-> C  <->  ( F : B --> C  /\  Fun  `' F ) )
52, 3, 43bitr4g 291 1  |-  ( A  =  B  ->  ( F : A -1-1-> C  <->  F : B -1-1-> C ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187    /\ wa 370    = wceq 1437   `'ccnv 4853   Fun wfun 5595   -->wf 5597   -1-1->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