Theorem f1fveq 7211

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

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1542   ∈ wcel 2114  –1-1→wf1 6490  ‘cfv 6493

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5232  ax-nul 5242  ax-pr 5371

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-id 5520  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-iota 6449  df-fun 6495  df-fn 6496  df-f 6497  df-f1 6498  df-fv 6501

This theorem is referenced by:  f1elima  7212  f1dom3fv3dif  7217  cocan1  7240  isof1oidb  7273  isosolem  7296  f1oiso  7300  weniso  7303  f1oweALT  7919  2dom  8971  xpdom2  9004  wemapwe  9612  fseqenlem1  9940  dfac12lem2  10061  infpssrlem4  10222  fin23lem28  10256  isf32lem7  10275  iundom2g  10456  canthnumlem  10565  canthwelem  10567  canthp1lem2  10570  pwfseqlem4  10579  seqf1olem1  13997  bitsinv2  16406  bitsf1  16409  sadasslem  16433  sadeq  16435  bitsuz  16437  eulerthlem2  16746  f1ocpbllem  17482  f1ovscpbl  17484  fthi  17881  f1omvdmvd  19412  odf1  19531  dprdf1o  20003  zntoslem  21549  iporthcom  21628  ply1scln0  22269  cnt0  23324  cnhaus  23332  imasdsf1olem  24351  imasf1oxmet  24353  dyadmbl  25580  vitalilem3  25590  dvcnvlem  25956  facth1  26145  usgredg2v  29313  mndlactf1o  33108  mndractf1o  33109  cycpmco2lem6  33210  erdszelem9  35400  cvmliftmolem1  35482  msubff1  35757  metf1o  38093  rngoisocnv  38319  laut11  40549  aks6d1c6lem3  42628  gicabl  43548  permac8prim  45462  fourierdlem50  46605  isuspgrim0lem  48384  uptrlem1  49700