Theorem f1fveq 7019

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398   = wceq 1533   ∈ wcel 2110  –1-1→wf1 6351  ‘cfv 6354

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793  ax-sep 5202  ax-nul 5209  ax-pr 5329

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3496  df-sbc 3772  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-nul 4291  df-if 4467  df-sn 4567  df-pr 4569  df-op 4573  df-uni 4838  df-br 5066  df-opab 5128  df-id 5459  df-xp 5560  df-rel 5561  df-cnv 5562  df-co 5563  df-dm 5564  df-iota 6313  df-fun 6356  df-fn 6357  df-f 6358  df-f1 6359  df-fv 6362

This theorem is referenced by:  f1elima  7020  f1dom3fv3dif  7025  cocan1  7046  isof1oidb  7076  isosolem  7099  f1oiso  7103  weniso  7106  f1oweALT  7672  2dom  8581  xpdom2  8611  wemapwe  9159  fseqenlem1  9449  dfac12lem2  9569  infpssrlem4  9727  fin23lem28  9761  isf32lem7  9780  iundom2g  9961  canthnumlem  10069  canthwelem  10071  canthp1lem2  10074  pwfseqlem4  10083  seqf1olem1  13408  bitsinv2  15791  bitsf1  15794  sadasslem  15818  sadeq  15820  bitsuz  15822  eulerthlem2  16118  f1ocpbllem  16796  f1ovscpbl  16798  fthi  17187  ghmf1  18386  f1omvdmvd  18570  odf1  18688  dprdf1o  19153  ply1scln0  20458  zntoslem  20702  iporthcom  20778  cnt0  21953  cnhaus  21961  imasdsf1olem  22982  imasf1oxmet  22984  dyadmbl  24200  vitalilem3  24210  dvcnvlem  24572  facth1  24757  usgredg2v  27008  cycpmco2lem6  30773  erdszelem9  32446  cvmliftmolem1  32528  msubff1  32803  metf1o  35029  rngoisocnv  35258  laut11  37221  gicabl  39697  fourierdlem50  42440