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

Theorem f1eq2 5602
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 5543 . . 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 5423 . 2  |-  ( F : A -1-1-> C  <->  ( F : A --> C  /\  Fun  `' F ) )
4 df-f1 5423 . 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 1369   `'ccnv 4839   Fun wfun 5412   -->wf 5414   -1-1->wf1 5415
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-12 1792  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1587  df-cleq 2436  df-fn 5421  df-f 5422  df-f1 5423
This theorem is referenced by:  f1oeq2  5633  f1eq123d  5636  brdomg  7320  marypha1lem  7683  fseqenlem1  8194  dfac12lem2  8313  dfac12lem3  8314  ackbij2  8412  iundom2g  8704  hashf1  12210  isuslgra  23271  isusgra  23272  ausisusgra  23279  usgra0  23289  uslgra1  23291  usgra1  23292  cusgraexilem2  23375  2trllemE  23452  constr1trl  23487  fargshiftf1  23523  usgrcyclnl2  23527  4cycl4dv  23553  eldioph2lem2  29099  usgra2pthlem1  30300  usgra2pth  30301
  Copyright terms: Public domain W3C validator