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

Theorem f1fveq 5786
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 5525 . . . . . . 7  |-  ( x  =  C  ->  ( F `  x )  =  ( F `  C ) )
21eqeq1d 2291 . . . . . 6  |-  ( x  =  C  ->  (
( F `  x
)  =  ( F `
 y )  <->  ( F `  C )  =  ( F `  y ) ) )
3 eqeq1 2289 . . . . . 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 5525 . . . . . . 7  |-  ( y  =  D  ->  ( F `  y )  =  ( F `  D ) )
76eqeq2d 2294 . . . . . 6  |-  ( y  =  D  ->  (
( F `  C
)  =  ( F `
 y )  <->  ( F `  C )  =  ( F `  D ) ) )
8 eqeq2 2292 . . . . . 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 5783 . . . . . . 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 2605 . . . . . 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 2851 . . 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 5525 . 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 1623    e. wcel 1684   A.wral 2543   -->wf 5251   -1-1->wf1 5252   ` cfv 5255
This theorem is referenced by:  f1elima  5787  cocan1  5801  isosolem  5844  f1oiso  5848  f1oweALT  5851  weniso  5852  2dom  6933  xpdom2  6957  wemapwe  7400  fseqenlem1  7651  dfac12lem2  7770  infpssrlem4  7932  fin23lem28  7966  isf32lem7  7985  iundom2g  8162  canthnumlem  8270  canthwelem  8272  canthp1lem2  8275  pwfseqlem4  8284  seqf1olem1  11085  bitsinv2  12634  bitsf1  12637  sadasslem  12661  sadeq  12663  bitsuz  12665  eulerthlem2  12850  f1ocpbllem  13426  f1ovscpbl  13428  fthi  13792  ghmf1  14711  odf1  14875  dprdf1o  15267  ply1scln0  16366  zntoslem  16510  iporthcom  16539  cnt0  17074  cnhaus  17082  imasdsf1olem  17937  imasf1oxmet  17939  dyadmbl  18955  vitalilem3  18965  dvcnvlem  19323  facth1  19550  erdszelem9  23730  cvmliftmolem1  23812  grpodlcan  25376  grpodivzer  25377  metf1o  26469  rngoisocnv  26612  gicabl  27263  f1omvdmvd  27386  laut11  30275
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-14 1688  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-sep 4141  ax-nul 4149  ax-pr 4214
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-eu 2147  df-mo 2148  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-ral 2548  df-rex 2549  df-rab 2552  df-v 2790  df-sbc 2992  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-sn 3646  df-pr 3647  df-op 3649  df-uni 3828  df-br 4024  df-opab 4078  df-id 4309  df-xp 4695  df-rel 4696  df-cnv 4697  df-co 4698  df-dm 4699  df-iota 5219  df-fun 5257  df-fn 5258  df-f 5259  df-f1 5260  df-fv 5263
  Copyright terms: Public domain W3C validator