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

Theorem f1fveq 7191
Description: Equality of function values for a one-to-one function. (Contributed by NM, 11-Feb-1997.)
Assertion
Ref Expression
f1fveq ((𝐹:𝐴1-1𝐵 ∧ (𝐶𝐴𝐷𝐴)) → ((𝐹𝐶) = (𝐹𝐷) ↔ 𝐶 = 𝐷))

Proof of Theorem f1fveq
StepHypRef Expression
1 f1veqaeq 7186 . 2 ((𝐹:𝐴1-1𝐵 ∧ (𝐶𝐴𝐷𝐴)) → ((𝐹𝐶) = (𝐹𝐷) → 𝐶 = 𝐷))
2 fveq2 6825 . 2 (𝐶 = 𝐷 → (𝐹𝐶) = (𝐹𝐷))
31, 2impbid1 224 1 ((𝐹:𝐴1-1𝐵 ∧ (𝐶𝐴𝐷𝐴)) → ((𝐹𝐶) = (𝐹𝐷) ↔ 𝐶 = 𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396   = wceq 1540  wcel 2105  1-1wf1 6476  cfv 6479
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2707  ax-sep 5243  ax-nul 5250  ax-pr 5372
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3404  df-v 3443  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4270  df-if 4474  df-sn 4574  df-pr 4576  df-op 4580  df-uni 4853  df-br 5093  df-opab 5155  df-id 5518  df-xp 5626  df-rel 5627  df-cnv 5628  df-co 5629  df-dm 5630  df-iota 6431  df-fun 6481  df-fn 6482  df-f 6483  df-f1 6484  df-fv 6487
This theorem is referenced by:  f1elima  7192  f1dom3fv3dif  7197  cocan1  7219  isof1oidb  7251  isosolem  7274  f1oiso  7278  weniso  7281  f1oweALT  7883  2dom  8895  xpdom2  8932  wemapwe  9554  fseqenlem1  9881  dfac12lem2  10001  infpssrlem4  10163  fin23lem28  10197  isf32lem7  10216  iundom2g  10397  canthnumlem  10505  canthwelem  10507  canthp1lem2  10510  pwfseqlem4  10519  seqf1olem1  13863  bitsinv2  16249  bitsf1  16252  sadasslem  16276  sadeq  16278  bitsuz  16280  eulerthlem2  16580  f1ocpbllem  17332  f1ovscpbl  17334  fthi  17731  ghmf1  18959  f1omvdmvd  19147  odf1  19265  dprdf1o  19730  zntoslem  20870  iporthcom  20946  ply1scln0  21568  cnt0  22603  cnhaus  22611  imasdsf1olem  23632  imasf1oxmet  23634  dyadmbl  24870  vitalilem3  24880  dvcnvlem  25246  facth1  25435  usgredg2v  27883  cycpmco2lem6  31685  erdszelem9  33460  cvmliftmolem1  33542  msubff1  33817  metf1o  36018  rngoisocnv  36244  laut11  38354  gicabl  41187  fourierdlem50  44033
  Copyright terms: Public domain W3C validator