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

Theorem f1fveq 6662
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 6657 . 2 ((𝐹:𝐴1-1𝐵 ∧ (𝐶𝐴𝐷𝐴)) → ((𝐹𝐶) = (𝐹𝐷) → 𝐶 = 𝐷))
2 fveq2 6332 . 2 (𝐶 = 𝐷 → (𝐹𝐶) = (𝐹𝐷))
31, 2impbid1 215 1 ((𝐹:𝐴1-1𝐵 ∧ (𝐶𝐴𝐷𝐴)) → ((𝐹𝐶) = (𝐹𝐷) ↔ 𝐶 = 𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 382   = wceq 1631  wcel 2145  1-1wf1 6028  cfv 6031
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-sep 4915  ax-nul 4923  ax-pr 5034
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 835  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ral 3066  df-rex 3067  df-rab 3070  df-v 3353  df-sbc 3588  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-nul 4064  df-if 4226  df-sn 4317  df-pr 4319  df-op 4323  df-uni 4575  df-br 4787  df-opab 4847  df-id 5157  df-xp 5255  df-rel 5256  df-cnv 5257  df-co 5258  df-dm 5259  df-iota 5994  df-fun 6033  df-fn 6034  df-f 6035  df-f1 6036  df-fv 6039
This theorem is referenced by:  f1elima  6663  f1dom3fv3dif  6668  cocan1  6689  isof1oidb  6717  isosolem  6740  f1oiso  6744  weniso  6747  f1oweALT  7299  2dom  8182  xpdom2  8211  wemapwe  8758  fseqenlem1  9047  dfac12lem2  9168  infpssrlem4  9330  fin23lem28  9364  isf32lem7  9383  iundom2g  9564  canthnumlem  9672  canthwelem  9674  canthp1lem2  9677  pwfseqlem4  9686  seqf1olem1  13047  bitsinv2  15373  bitsf1  15376  sadasslem  15400  sadeq  15402  bitsuz  15404  eulerthlem2  15694  f1ocpbllem  16392  f1ovscpbl  16394  fthi  16785  ghmf1  17897  f1omvdmvd  18070  odf1  18186  dprdf1o  18639  ply1scln0  19876  zntoslem  20120  iporthcom  20197  cnt0  21371  cnhaus  21379  imasdsf1olem  22398  imasf1oxmet  22400  dyadmbl  23588  vitalilem3  23598  dvcnvlem  23959  facth1  24144  usgredg2v  26341  erdszelem9  31519  cvmliftmolem1  31601  msubff1  31791  metf1o  33883  rngoisocnv  34112  laut11  35894  gicabl  38195  fourierdlem50  40890
  Copyright terms: Public domain W3C validator