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

Theorem f1eq3 5793
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 5730 . . 3  |-  ( A  =  B  ->  ( F : C --> A  <->  F : C
--> B ) )
21anbi1d 709 . 2  |-  ( A  =  B  ->  (
( F : C --> A  /\  Fun  `' F
)  <->  ( F : C
--> B  /\  Fun  `' F ) ) )
3 df-f1 5606 . 2  |-  ( F : C -1-1-> A  <->  ( F : C --> A  /\  Fun  `' F ) )
4 df-f1 5606 . 2  |-  ( F : C -1-1-> B  <->  ( F : C --> B  /\  Fun  `' F ) )
52, 3, 43bitr4g 291 1  |-  ( A  =  B  ->  ( F : C -1-1-> A  <->  F : C -1-1-> B ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187    /\ wa 370    = wceq 1437   `'ccnv 4852   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 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2408  df-cleq 2414  df-clel 2417  df-in 3443  df-ss 3450  df-f 5605  df-f1 5606
This theorem is referenced by:  f1oeq3  5824  f1eq123d  5826  tposf12  7009  brdomg  7590  pwfseq  9096  f1linds  19381  isuslgra  25068  isusgra  25069  isusgra0  25072  usgraop  25075  cusgraexilem2  25193  diaf1oN  34667  isusgr0  39036  usgr1vr  39105  usgrexi  39262
  Copyright terms: Public domain W3C validator