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

Theorem f1fveq 6149
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
StepHypRef Expression
1 f1veqaeq 6147 . 2  |-  ( ( F : A -1-1-> B  /\  ( C  e.  A  /\  D  e.  A
) )  ->  (
( F `  C
)  =  ( F `
 D )  ->  C  =  D )
)
2 fveq2 5857 . 2  |-  ( C  =  D  ->  ( F `  C )  =  ( F `  D ) )
31, 2impbid1 203 1  |-  ( ( F : A -1-1-> B  /\  ( C  e.  A  /\  D  e.  A
) )  ->  (
( F `  C
)  =  ( F `
 D )  <->  C  =  D ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369    = wceq 1374    e. wcel 1762   -1-1->wf1 5576   ` cfv 5579
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-9 1766  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438  ax-sep 4561  ax-nul 4569  ax-pr 4679
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 970  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-eu 2272  df-mo 2273  df-clab 2446  df-cleq 2452  df-clel 2455  df-nfc 2610  df-ne 2657  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3108  df-sbc 3325  df-dif 3472  df-un 3474  df-in 3476  df-ss 3483  df-nul 3779  df-if 3933  df-sn 4021  df-pr 4023  df-op 4027  df-uni 4239  df-br 4441  df-opab 4499  df-id 4788  df-xp 4998  df-rel 4999  df-cnv 5000  df-co 5001  df-dm 5002  df-iota 5542  df-fun 5581  df-fn 5582  df-f 5583  df-f1 5584  df-fv 5587
This theorem is referenced by:  f1elima  6150  f1dom3fv3dif  6154  cocan1  6173  isosolem  6222  f1oiso  6226  weniso  6229  f1oweALT  6758  2dom  7578  xpdom2  7602  wemapwe  8128  wemapweOLD  8129  fseqenlem1  8394  dfac12lem2  8513  infpssrlem4  8675  fin23lem28  8709  isf32lem7  8728  iundom2g  8904  canthnumlem  9015  canthwelem  9017  canthp1lem2  9020  pwfseqlem4  9029  seqf1olem1  12102  bitsinv2  13941  bitsf1  13944  sadasslem  13968  sadeq  13970  bitsuz  13972  eulerthlem2  14160  f1ocpbllem  14768  f1ovscpbl  14770  fthi  15134  ghmf1  16083  f1omvdmvd  16257  odf1  16373  dprdf1o  16862  ply1scln0  18096  zntoslem  18355  iporthcom  18430  cnt0  19606  cnhaus  19614  imasdsf1olem  20604  imasf1oxmet  20606  dyadmbl  21737  vitalilem3  21747  dvcnvlem  22105  facth1  22293  usgraidx2v  24055  wlkdvspthlem  24271  cyclnspth  24293  usgrcyclnl2  24303  erdszelem9  28269  cvmliftmolem1  28352  metf1o  29838  rngoisocnv  29974  gicabl  30640  fourierdlem50  31412  laut11  34757
  Copyright terms: Public domain W3C validator