Theorem f1fveq 7044

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

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1542   ∈ wcel 2114  –1-1→wf1 6347  ‘cfv 6350

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 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2162  ax-12 2179  ax-ext 2711  ax-sep 5177  ax-nul 5184  ax-pr 5306

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2075  df-mo 2541  df-eu 2571  df-clab 2718  df-cleq 2731  df-clel 2812  df-nfc 2882  df-ral 3059  df-rex 3060  df-v 3402  df-sbc 3686  df-dif 3856  df-un 3858  df-in 3860  df-ss 3870  df-nul 4222  df-if 4425  df-sn 4527  df-pr 4529  df-op 4533  df-uni 4807  df-br 5041  df-opab 5103  df-id 5439  df-xp 5541  df-rel 5542  df-cnv 5543  df-co 5544  df-dm 5545  df-iota 6308  df-fun 6352  df-fn 6353  df-f 6354  df-f1 6355  df-fv 6358

This theorem is referenced by:  f1elima  7045  f1dom3fv3dif  7050  cocan1  7071  isof1oidb  7103  isosolem  7126  f1oiso  7130  weniso  7133  f1oweALT  7711  2dom  8642  xpdom2  8674  wemapwe  9246  fseqenlem1  9537  dfac12lem2  9657  infpssrlem4  9819  fin23lem28  9853  isf32lem7  9872  iundom2g  10053  canthnumlem  10161  canthwelem  10163  canthp1lem2  10166  pwfseqlem4  10175  seqf1olem1  13514  bitsinv2  15899  bitsf1  15902  sadasslem  15926  sadeq  15928  bitsuz  15930  eulerthlem2  16232  f1ocpbllem  16913  f1ovscpbl  16915  fthi  17306  ghmf1  18518  f1omvdmvd  18702  odf1  18820  dprdf1o  19286  zntoslem  20388  iporthcom  20464  ply1scln0  21079  cnt0  22110  cnhaus  22118  imasdsf1olem  23139  imasf1oxmet  23141  dyadmbl  24365  vitalilem3  24375  dvcnvlem  24741  facth1  24930  usgredg2v  27182  cycpmco2lem6  30988  erdszelem9  32745  cvmliftmolem1  32827  msubff1  33102  metf1o  35569  rngoisocnv  35795  laut11  37756  gicabl  40537  fourierdlem50  43280