Theorem f1fveq 7196

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1541   ∈ wcel 2111  –1-1→wf1 6478  ‘cfv 6481

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-sep 5232  ax-nul 5242  ax-pr 5368

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-ne 2929  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-ss 3914  df-nul 4281  df-if 4473  df-sn 4574  df-pr 4576  df-op 4580  df-uni 4857  df-br 5090  df-opab 5152  df-id 5509  df-xp 5620  df-rel 5621  df-cnv 5622  df-co 5623  df-dm 5624  df-iota 6437  df-fun 6483  df-fn 6484  df-f 6485  df-f1 6486  df-fv 6489

This theorem is referenced by:  f1elima  7197  f1dom3fv3dif  7202  cocan1  7225  isof1oidb  7258  isosolem  7281  f1oiso  7285  weniso  7288  f1oweALT  7904  2dom  8952  xpdom2  8985  wemapwe  9587  fseqenlem1  9915  dfac12lem2  10036  infpssrlem4  10197  fin23lem28  10231  isf32lem7  10250  iundom2g  10431  canthnumlem  10539  canthwelem  10541  canthp1lem2  10544  pwfseqlem4  10553  seqf1olem1  13948  bitsinv2  16354  bitsf1  16357  sadasslem  16381  sadeq  16383  bitsuz  16385  eulerthlem2  16693  f1ocpbllem  17428  f1ovscpbl  17430  fthi  17827  f1omvdmvd  19355  odf1  19474  dprdf1o  19946  zntoslem  21493  iporthcom  21572  ply1scln0  22206  cnt0  23261  cnhaus  23269  imasdsf1olem  24288  imasf1oxmet  24290  dyadmbl  25528  vitalilem3  25538  dvcnvlem  25907  facth1  26099  usgredg2v  29205  mndlactf1o  33011  mndractf1o  33012  cycpmco2lem6  33100  erdszelem9  35243  cvmliftmolem1  35325  msubff1  35600  metf1o  37803  rngoisocnv  38029  laut11  40133  aks6d1c6lem3  42213  gicabl  43140  permac8prim  45055  fourierdlem50  46202  isuspgrim0lem  47932  uptrlem1  49250