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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1570   ∈ wcel 2145  –1-1→wf1 6530  ‘cfv 6533

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-sep 5251  ax-nul 5263  ax-pr 5398

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  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-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-id 5550  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-iota 6489  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fv 6541

This theorem is used by:  f1elima  7261  f1dom3fv3dif  7266  cocan1  7293  isof1oidb  7326  isosolem  7349  f1oiso  7353  weniso  7358  f1oweALT  7970  2dom  9038  xpdom2  9071  wemapwe  9677  fseqenlem1  10028  dfac12lem2  10148  infpssrlem4  10309  fin23lem28  10343  isf32lem7  10362  iundom2g  10549  canthnumlem  10658  canthwelem  10660  canthp1lem2  10663  pwfseqlem4  10672  seqf1olem1  14106  bitsinv2  16534  bitsf1  16537  sadasslem  16561  sadeq  16563  bitsuz  16565  eulerthlem2  16874  f1ocpbllem  17611  f1ovscpbl  17613  fthi  18010  f1omvdmvd  19571  odf1  19690  dprdf1o  20162  zntoslem  21770  iporthcom  21849  ply1scln0  22518  cnt0  23572  cnhaus  23580  imasdsf1olem  24600  imasf1oxmet  24602  dyadmbl  25829  vitalilem3  25839  dvcnvlem  26204  facth1  26393  usgredg2v  29688  mndlactf1o  33471  mndractf1o  33472  cycpmco2lem6  33572  erdszelem9  35779  cvmliftmolem1  35861  msubff1  36136  metf1o  38506  rngoisocnv  38732  laut11  40960  aks6d1c6lem3  43039  gicabl  43941  permac8prim  45838  fourierdlem50  46985  isuspgrim0lem  48810  uptrlem1  50137