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

Theorem f1fveq 5802
Description: Equality of function values for a one-to-one function. (Contributed by NM, 11-Feb-1997.)
Assertion
Ref Expression
f1fveq  |-  ( ( F : A -1-1-> B  /\  ( C  e.  A  /\  D  e.  A
) )  ->  (
( F `  C
)  =  ( F `
 D )  <->  C  =  D ) )

Proof of Theorem f1fveq
Dummy variables  x  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fveq2 5541 . . . . . . 7  |-  ( x  =  C  ->  ( F `  x )  =  ( F `  C ) )
21eqeq1d 2304 . . . . . 6  |-  ( x  =  C  ->  (
( F `  x
)  =  ( F `
 y )  <->  ( F `  C )  =  ( F `  y ) ) )
3 eqeq1 2302 . . . . . 6  |-  ( x  =  C  ->  (
x  =  y  <->  C  =  y ) )
42, 3imbi12d 311 . . . . 5  |-  ( x  =  C  ->  (
( ( F `  x )  =  ( F `  y )  ->  x  =  y )  <->  ( ( F `
 C )  =  ( F `  y
)  ->  C  =  y ) ) )
54imbi2d 307 . . . 4  |-  ( x  =  C  ->  (
( F : A -1-1-> B  ->  ( ( F `
 x )  =  ( F `  y
)  ->  x  =  y ) )  <->  ( F : A -1-1-> B  ->  ( ( F `  C )  =  ( F `  y )  ->  C  =  y ) ) ) )
6 fveq2 5541 . . . . . . 7  |-  ( y  =  D  ->  ( F `  y )  =  ( F `  D ) )
76eqeq2d 2307 . . . . . 6  |-  ( y  =  D  ->  (
( F `  C
)  =  ( F `
 y )  <->  ( F `  C )  =  ( F `  D ) ) )
8 eqeq2 2305 . . . . . 6  |-  ( y  =  D  ->  ( C  =  y  <->  C  =  D ) )
97, 8imbi12d 311 . . . . 5  |-  ( y  =  D  ->  (
( ( F `  C )  =  ( F `  y )  ->  C  =  y )  <->  ( ( F `
 C )  =  ( F `  D
)  ->  C  =  D ) ) )
109imbi2d 307 . . . 4  |-  ( y  =  D  ->  (
( F : A -1-1-> B  ->  ( ( F `
 C )  =  ( F `  y
)  ->  C  =  y ) )  <->  ( F : A -1-1-> B  ->  ( ( F `  C )  =  ( F `  D )  ->  C  =  D ) ) ) )
11 dff13 5799 . . . . . . 7  |-  ( F : A -1-1-> B  <->  ( F : A --> B  /\  A. x  e.  A  A. y  e.  A  (
( F `  x
)  =  ( F `
 y )  ->  x  =  y )
) )
1211simprbi 450 . . . . . 6  |-  ( F : A -1-1-> B  ->  A. x  e.  A  A. y  e.  A  ( ( F `  x )  =  ( F `  y )  ->  x  =  y ) )
13 rsp2 2618 . . . . . 6  |-  ( A. x  e.  A  A. y  e.  A  (
( F `  x
)  =  ( F `
 y )  ->  x  =  y )  ->  ( ( x  e.  A  /\  y  e.  A )  ->  (
( F `  x
)  =  ( F `
 y )  ->  x  =  y )
) )
1412, 13syl 15 . . . . 5  |-  ( F : A -1-1-> B  -> 
( ( x  e.  A  /\  y  e.  A )  ->  (
( F `  x
)  =  ( F `
 y )  ->  x  =  y )
) )
1514com12 27 . . . 4  |-  ( ( x  e.  A  /\  y  e.  A )  ->  ( F : A -1-1-> B  ->  ( ( F `
 x )  =  ( F `  y
)  ->  x  =  y ) ) )
165, 10, 15vtocl2ga 2864 . . 3  |-  ( ( C  e.  A  /\  D  e.  A )  ->  ( F : A -1-1-> B  ->  ( ( F `
 C )  =  ( F `  D
)  ->  C  =  D ) ) )
1716impcom 419 . 2  |-  ( ( F : A -1-1-> B  /\  ( C  e.  A  /\  D  e.  A
) )  ->  (
( F `  C
)  =  ( F `
 D )  ->  C  =  D )
)
18 fveq2 5541 . 2  |-  ( C  =  D  ->  ( F `  C )  =  ( F `  D ) )
1917, 18impbid1 194 1  |-  ( ( F : A -1-1-> B  /\  ( C  e.  A  /\  D  e.  A
) )  ->  (
( F `  C
)  =  ( F `
 D )  <->  C  =  D ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358    = wceq 1632    e. wcel 1696   A.wral 2556   -->wf 5267   -1-1->wf1 5268   ` cfv 5271
This theorem is referenced by:  f1elima  5803  cocan1  5817  isosolem  5860  f1oiso  5864  f1oweALT  5867  weniso  5868  2dom  6949  xpdom2  6973  wemapwe  7416  fseqenlem1  7667  dfac12lem2  7786  infpssrlem4  7948  fin23lem28  7982  isf32lem7  8001  iundom2g  8178  canthnumlem  8286  canthwelem  8288  canthp1lem2  8291  pwfseqlem4  8300  seqf1olem1  11101  bitsinv2  12650  bitsf1  12653  sadasslem  12677  sadeq  12679  bitsuz  12681  eulerthlem2  12866  f1ocpbllem  13442  f1ovscpbl  13444  fthi  13808  ghmf1  14727  odf1  14891  dprdf1o  15283  ply1scln0  16382  zntoslem  16526  iporthcom  16555  cnt0  17090  cnhaus  17098  imasdsf1olem  17953  imasf1oxmet  17955  dyadmbl  18971  vitalilem3  18981  dvcnvlem  19339  facth1  19566  erdszelem9  23745  cvmliftmolem1  23827  grpodlcan  25479  grpodivzer  25480  metf1o  26572  rngoisocnv  26715  gicabl  27366  f1omvdmvd  27489  wlkdvspthlem  28365  cyclnspth  28376  usgrcyclnl2  28387  laut11  30897
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-14 1700  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277  ax-sep 4157  ax-nul 4165  ax-pr 4230
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-eu 2160  df-mo 2161  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ne 2461  df-ral 2561  df-rex 2562  df-rab 2565  df-v 2803  df-sbc 3005  df-dif 3168  df-un 3170  df-in 3172  df-ss 3179  df-nul 3469  df-if 3579  df-sn 3659  df-pr 3660  df-op 3662  df-uni 3844  df-br 4040  df-opab 4094  df-id 4325  df-xp 4711  df-rel 4712  df-cnv 4713  df-co 4714  df-dm 4715  df-iota 5235  df-fun 5273  df-fn 5274  df-f 5275  df-f1 5276  df-fv 5279
  Copyright terms: Public domain W3C validator