Theorem f1fveq 7263

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 394   = wceq 1539   ∈ wcel 2104  –1-1→wf1 6539  ‘cfv 6542

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701  ax-sep 5298  ax-nul 5305  ax-pr 5426

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-ne 2939  df-ral 3060  df-rex 3069  df-rab 3431  df-v 3474  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-opab 5210  df-id 5573  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fv 6550

This theorem is referenced by:  f1elima  7264  f1dom3fv3dif  7269  cocan1  7291  isof1oidb  7323  isosolem  7346  f1oiso  7350  weniso  7353  f1oweALT  7961  2dom  9032  xpdom2  9069  wemapwe  9694  fseqenlem1  10021  dfac12lem2  10141  infpssrlem4  10303  fin23lem28  10337  isf32lem7  10356  iundom2g  10537  canthnumlem  10645  canthwelem  10647  canthp1lem2  10650  pwfseqlem4  10659  seqf1olem1  14011  bitsinv2  16388  bitsf1  16391  sadasslem  16415  sadeq  16417  bitsuz  16419  eulerthlem2  16719  f1ocpbllem  17474  f1ovscpbl  17476  fthi  17873  f1omvdmvd  19352  odf1  19471  dprdf1o  19943  zntoslem  21331  iporthcom  21407  ply1scln0  22034  cnt0  23070  cnhaus  23078  imasdsf1olem  24099  imasf1oxmet  24101  dyadmbl  25349  vitalilem3  25359  dvcnvlem  25728  facth1  25917  usgredg2v  28751  cycpmco2lem6  32560  erdszelem9  34488  cvmliftmolem1  34570  msubff1  34845  metf1o  36926  rngoisocnv  37152  laut11  39260  gicabl  42143  fourierdlem50  45170