Theorem f1fveq 7282

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1540   ∈ wcel 2108  –1-1→wf1 6558  ‘cfv 6561

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 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-opab 5206  df-id 5578  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fv 6569

This theorem is referenced by:  f1elima  7283  f1dom3fv3dif  7288  cocan1  7311  isof1oidb  7344  isosolem  7367  f1oiso  7371  weniso  7374  f1oweALT  7997  2dom  9070  xpdom2  9107  wemapwe  9737  fseqenlem1  10064  dfac12lem2  10185  infpssrlem4  10346  fin23lem28  10380  isf32lem7  10399  iundom2g  10580  canthnumlem  10688  canthwelem  10690  canthp1lem2  10693  pwfseqlem4  10702  seqf1olem1  14082  bitsinv2  16480  bitsf1  16483  sadasslem  16507  sadeq  16509  bitsuz  16511  eulerthlem2  16819  f1ocpbllem  17569  f1ovscpbl  17571  fthi  17965  f1omvdmvd  19461  odf1  19580  dprdf1o  20052  zntoslem  21575  iporthcom  21653  ply1scln0  22295  cnt0  23354  cnhaus  23362  imasdsf1olem  24383  imasf1oxmet  24385  dyadmbl  25635  vitalilem3  25645  dvcnvlem  26014  facth1  26206  usgredg2v  29244  mndlactf1o  33035  mndractf1o  33036  cycpmco2lem6  33151  erdszelem9  35204  cvmliftmolem1  35286  msubff1  35561  metf1o  37762  rngoisocnv  37988  laut11  40088  aks6d1c6lem3  42173  gicabl  43111  fourierdlem50  46171  isuspgrim0lem  47871