Theorem f1fveq 7270

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1569   ∈ wcel 2144  –1-1→wf1 6540  ‘cfv 6543

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pr 5391

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3897  df-dif 4046  df-in 4090  df-un 4150  df-nul 4278  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-opab 5167  df-id 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-iota 6497  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fv 6551

This theorem is used by:  f1elima  7271  f1dom3fv3dif  7276  cocan1  7303  isof1oidb  7336  isosolem  7359  f1oiso  7363  weniso  7368  f1oweALT  7988  2dom  9066  xpdom2  9099  wemapwe  9705  fseqenlem1  10110  dfac12lem2  10230  infpssrlem4  10391  fin23lem28  10425  isf32lem7  10444  iundom2g  10631  canthnumlem  10740  canthwelem  10742  canthp1lem2  10745  pwfseqlem4  10754  seqf1olem1  14191  bitsinv2  16622  bitsf1  16625  sadasslem  16649  sadeq  16651  bitsuz  16653  eulerthlem2  16968  f1ocpbllem  17705  f1ovscpbl  17707  fthi  18104  f1omvdmvd  19666  odf1  19785  dprdf1o  20257  zntoslem  21871  iporthcom  21950  ply1scln0  22619  cnt0  23673  cnhaus  23681  imasdsf1olem  24701  imasf1oxmet  24703  dyadmbl  25930  vitalilem3  25940  dvcnvlem  26305  facth1  26494  usgredg2v  29817  mndlactf1o  33641  mndractf1o  33642  cycpmco2lem6  33742  erdszelem9  36082  cvmliftmolem1  36164  msubff1  36439  mh-inf3f1  37453  metf1o  38826  rngoisocnv  39052  laut11  41280  aks6d1c6lem3  43359  gicabl  44238  permac8prim  46140  fourierdlem50  47302  isuspgrim0lem  49127  uptrlem1  50462