Theorem f1fveq 7281

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 7276	. 2 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ (𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴)) → ((𝐹‘𝐶) = (𝐹‘𝐷) → 𝐶 = 𝐷))
2		fveq2 6906	. 2 ⊢ (𝐶 = 𝐷 → (𝐹‘𝐶) = (𝐹‘𝐷))
3	1, 2	impbid1 225	1 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ (𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴)) → ((𝐹‘𝐶) = (𝐹‘𝐷) ↔ 𝐶 = 𝐷))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1536   ∈ wcel 2105  –1-1→wf1 6559  ‘cfv 6562

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pr 5437

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-ne 2938  df-ral 3059  df-rex 3068  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-opab 5210  df-id 5582  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-f1 6567  df-fv 6570

This theorem is referenced by:  f1elima  7282  f1dom3fv3dif  7287  cocan1  7310  isof1oidb  7343  isosolem  7366  f1oiso  7370  weniso  7373  f1oweALT  7995  2dom  9068  xpdom2  9105  wemapwe  9734  fseqenlem1  10061  dfac12lem2  10182  infpssrlem4  10343  fin23lem28  10377  isf32lem7  10396  iundom2g  10577  canthnumlem  10685  canthwelem  10687  canthp1lem2  10690  pwfseqlem4  10699  seqf1olem1  14078  bitsinv2  16476  bitsf1  16479  sadasslem  16503  sadeq  16505  bitsuz  16507  eulerthlem2  16815  f1ocpbllem  17570  f1ovscpbl  17572  fthi  17971  f1omvdmvd  19475  odf1  19594  dprdf1o  20066  zntoslem  21592  iporthcom  21670  ply1scln0  22310  cnt0  23369  cnhaus  23377  imasdsf1olem  24398  imasf1oxmet  24400  dyadmbl  25648  vitalilem3  25658  dvcnvlem  26028  facth1  26220  usgredg2v  29258  mndlactf1o  33017  mndractf1o  33018  cycpmco2lem6  33133  erdszelem9  35183  cvmliftmolem1  35265  msubff1  35540  metf1o  37741  rngoisocnv  37967  laut11  40068  aks6d1c6lem3  42153  gicabl  43087  fourierdlem50  46111  isuspgrim0lem  47808