Theorem f1fveq 7266

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 7260	. 2 ⊢ ((𝐹:𝐴–1-1→𝐵 ∧ (𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴)) → ((𝐹‘𝐶) = (𝐹‘𝐷) → 𝐶 = 𝐷))
2		fveq2 6885	. 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 6535  ‘cfv 6538

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 2733  ax-sep 5249  ax-nul 5260  ax-pr 5391

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 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  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 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fv 6546

This theorem is used by:  f1elima  7267  f1dom3fv3dif  7272  cocan1  7299  isof1oidb  7332  isosolem  7355  f1oiso  7359  weniso  7364  f1oweALT  7984  2dom  9058  xpdom2  9091  wemapwe  9698  fseqenlem1  10103  dfac12lem2  10223  infpssrlem4  10384  fin23lem28  10418  isf32lem7  10437  iundom2g  10624  canthnumlem  10733  canthwelem  10735  canthp1lem2  10738  pwfseqlem4  10747  seqf1olem1  14184  bitsinv2  16613  bitsf1  16616  sadasslem  16640  sadeq  16642  bitsuz  16644  eulerthlem2  16959  f1ocpbllem  17696  f1ovscpbl  17698  fthi  18095  f1omvdmvd  19657  odf1  19776  dprdf1o  20248  zntoslem  21862  iporthcom  21941  ply1scln0  22610  cnt0  23664  cnhaus  23672  imasdsf1olem  24692  imasf1oxmet  24694  dyadmbl  25921  vitalilem3  25931  dvcnvlem  26296  facth1  26485  usgredg2v  29808  mndlactf1o  33591  mndractf1o  33592  cycpmco2lem6  33692  erdszelem9  35964  cvmliftmolem1  36046  msubff1  36321  mh-inf3f1  37329  metf1o  38689  rngoisocnv  38915  laut11  41143  aks6d1c6lem3  43222  gicabl  44100  permac8prim  46003  fourierdlem50  47165  isuspgrim0lem  48990  uptrlem1  50317