Theorem f1fveq 7218

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

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

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 5243  ax-nul 5253  ax-pr 5379

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 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-id 5527  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-iota 6456  df-fun 6502  df-fn 6503  df-f 6504  df-f1 6505  df-fv 6508

This theorem is referenced by:  f1elima  7219  f1dom3fv3dif  7224  cocan1  7247  isof1oidb  7280  isosolem  7303  f1oiso  7307  weniso  7310  f1oweALT  7926  2dom  8979  xpdom2  9012  wemapwe  9618  fseqenlem1  9946  dfac12lem2  10067  infpssrlem4  10228  fin23lem28  10262  isf32lem7  10281  iundom2g  10462  canthnumlem  10571  canthwelem  10573  canthp1lem2  10576  pwfseqlem4  10585  seqf1olem1  13976  bitsinv2  16382  bitsf1  16385  sadasslem  16409  sadeq  16411  bitsuz  16413  eulerthlem2  16721  f1ocpbllem  17457  f1ovscpbl  17459  fthi  17856  f1omvdmvd  19384  odf1  19503  dprdf1o  19975  zntoslem  21523  iporthcom  21602  ply1scln0  22246  cnt0  23302  cnhaus  23310  imasdsf1olem  24329  imasf1oxmet  24331  dyadmbl  25569  vitalilem3  25579  dvcnvlem  25948  facth1  26140  usgredg2v  29312  mndlactf1o  33123  mndractf1o  33124  cycpmco2lem6  33225  erdszelem9  35415  cvmliftmolem1  35497  msubff1  35772  metf1o  38006  rngoisocnv  38232  laut11  40462  aks6d1c6lem3  42542  gicabl  43456  permac8prim  45370  fourierdlem50  46514  isuspgrim0lem  48253  uptrlem1  49569