Theorem f1fveq 7260

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400   = wceq 1570   ∈ wcel 2143  –1-1→wf1 6533  ‘cfv 6536

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5257  ax-nul 5269  ax-pr 5404

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-ne 2959  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4488  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-br 5110  df-opab 5174  df-id 5556  df-xp 5667  df-rel 5668  df-cnv 5669  df-co 5670  df-dm 5671  df-iota 6492  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fv 6544

This theorem is referenced by:  f1elima  7261  f1dom3fv3dif  7266  cocan1  7289  isof1oidb  7322  isosolem  7345  f1oiso  7349  weniso  7352  f1oweALT  7965  2dom  9023  xpdom2  9056  wemapwe  9662  fseqenlem1  10004  dfac12lem2  10124  infpssrlem4  10285  fin23lem28  10319  isf32lem7  10338  iundom2g  10519  canthnumlem  10628  canthwelem  10630  canthp1lem2  10633  pwfseqlem4  10642  seqf1olem1  14073  bitsinv2  16496  bitsf1  16499  sadasslem  16523  sadeq  16525  bitsuz  16527  eulerthlem2  16836  f1ocpbllem  17573  f1ovscpbl  17575  fthi  17972  f1omvdmvd  19508  odf1  19627  dprdf1o  20099  zntoslem  21706  iporthcom  21785  ply1scln0  22452  cnt0  23503  cnhaus  23511  imasdsf1olem  24530  imasf1oxmet  24532  dyadmbl  25759  vitalilem3  25769  dvcnvlem  26135  facth1  26324  usgredg2v  29577  mndlactf1o  33350  mndractf1o  33351  cycpmco2lem6  33451  erdszelem9  35691  cvmliftmolem1  35773  msubff1  36048  metf1o  38406  rngoisocnv  38632  laut11  40860  aks6d1c6lem3  42939  gicabl  43826  permac8prim  45723  fourierdlem50  46870  isuspgrim0lem  48658  uptrlem1  49988