Theorem f1fveq 7206

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

Step	Hyp	Ref	Expression
1		f1veqaeq 7200	. 2 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ (𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴)) → ((𝐹‘𝐶) = (𝐹‘𝐷) → 𝐶 = 𝐷))
2		fveq2 6827	. 2 ⊢ (𝐶 = 𝐷 → (𝐹‘𝐶) = (𝐹‘𝐷))
3	1, 2	impbid1 226	1 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ (𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴)) → ((𝐹‘𝐶) = (𝐹‘𝐷) ↔ 𝐶 = 𝐷))

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396   = wceq 1547   ∈ wcel 2119  –1-1→wf1 6482  ‘cfv 6485

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2711  ax-sep 5218  ax-nul 5228  ax-pr 5362

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2718  df-cleq 2731  df-clel 2814  df-ne 2935  df-ral 3054  df-rex 3064  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4262  df-if 4455  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-br 5073  df-opab 5135  df-id 5513  df-xp 5624  df-rel 5625  df-cnv 5626  df-co 5627  df-dm 5628  df-iota 6441  df-fun 6487  df-fn 6488  df-f 6489  df-f1 6490  df-fv 6493

This theorem is referenced by:  f1elima  7207  f1dom3fv3dif  7212  cocan1  7235  isof1oidb  7268  isosolem  7291  f1oiso  7295  weniso  7298  f1oweALT  7914  2dom  8967  xpdom2  9000  wemapwe  9609  fseqenlem1  9937  dfac12lem2  10058  infpssrlem4  10219  fin23lem28  10253  isf32lem7  10272  iundom2g  10453  canthnumlem  10562  canthwelem  10564  canthp1lem2  10567  pwfseqlem4  10576  seqf1olem1  13994  bitsinv2  16403  bitsf1  16406  sadasslem  16430  sadeq  16432  bitsuz  16434  eulerthlem2  16743  f1ocpbllem  17479  f1ovscpbl  17481  fthi  17878  f1omvdmvd  19409  odf1  19528  dprdf1o  20000  zntoslem  21531  iporthcom  21610  ply1scln0  22277  cnt0  23329  cnhaus  23337  imasdsf1olem  24356  imasf1oxmet  24358  dyadmbl  25585  vitalilem3  25595  dvcnvlem  25961  facth1  26150  usgredg2v  29314  mndlactf1o  33109  mndractf1o  33110  cycpmco2lem6  33212  erdszelem9  35427  cvmliftmolem1  35509  msubff1  35784  metf1o  38122  rngoisocnv  38348  laut11  40578  aks6d1c6lem3  42657  gicabl  43544  permac8prim  45458  fourierdlem50  46599  isuspgrim0lem  48384  uptrlem1  49700