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

Theorem f1eq3 5759
Description: Equality theorem for one-to-one functions. (Contributed by NM, 10-Feb-1997.)
Assertion
Ref Expression
f1eq3  |-  ( A  =  B  ->  ( F : C -1-1-> A  <->  F : C -1-1-> B ) )

Proof of Theorem f1eq3
StepHypRef Expression
1 feq3 5694 . . 3  |-  ( A  =  B  ->  ( F : C --> A  <->  F : C
--> B ) )
21anbi1d 716 . 2  |-  ( A  =  B  ->  (
( F : C --> A  /\  Fun  `' F
)  <->  ( F : C
--> B  /\  Fun  `' F ) ) )
3 df-f1 5566 . 2  |-  ( F : C -1-1-> A  <->  ( F : C --> A  /\  Fun  `' F ) )
4 df-f1 5566 . 2  |-  ( F : C -1-1-> B  <->  ( F : C --> B  /\  Fun  `' F ) )
52, 3, 43bitr4g 296 1  |-  ( A  =  B  ->  ( F : C -1-1-> A  <->  F : C -1-1-> B ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 189    /\ wa 375    = wceq 1448   `'ccnv 4811   Fun wfun 5555   -->wf 5557   -1-1->wf1 5558
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1673  ax-4 1686  ax-5 1762  ax-6 1809  ax-7 1855  ax-10 1919  ax-11 1924  ax-12 1937  ax-13 2092  ax-ext 2432
This theorem depends on definitions:  df-bi 190  df-an 377  df-tru 1451  df-ex 1668  df-nf 1672  df-sb 1802  df-clab 2439  df-cleq 2445  df-clel 2448  df-in 3379  df-ss 3386  df-f 5565  df-f1 5566
This theorem is referenced by:  f1oeq3  5790  f1eq123d  5792  tposf12  6985  brdomg  7566  pwfseq  9076  f1linds  19394  isuslgra  25082  isusgra  25083  isusgra0  25086  usgraop  25089  cusgraexilem2  25207  diaf1oN  34700  isusgrs  39343  usgr1vr  39431  usgrexi  39608
  Copyright terms: Public domain W3C validator