Theorem f1fveq 7022

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

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398   = wceq 1537   ∈ wcel 2114  –1-1→wf1 6354  ‘cfv 6357

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795  ax-sep 5205  ax-nul 5212  ax-pr 5332

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-ral 3145  df-rex 3146  df-rab 3149  df-v 3498  df-sbc 3775  df-dif 3941  df-un 3943  df-in 3945  df-ss 3954  df-nul 4294  df-if 4470  df-sn 4570  df-pr 4572  df-op 4576  df-uni 4841  df-br 5069  df-opab 5131  df-id 5462  df-xp 5563  df-rel 5564  df-cnv 5565  df-co 5566  df-dm 5567  df-iota 6316  df-fun 6359  df-fn 6360  df-f 6361  df-f1 6362  df-fv 6365

This theorem is referenced by:  f1elima  7023  f1dom3fv3dif  7028  cocan1  7049  isof1oidb  7079  isosolem  7102  f1oiso  7106  weniso  7109  f1oweALT  7675  2dom  8584  xpdom2  8614  wemapwe  9162  fseqenlem1  9452  dfac12lem2  9572  infpssrlem4  9730  fin23lem28  9764  isf32lem7  9783  iundom2g  9964  canthnumlem  10072  canthwelem  10074  canthp1lem2  10077  pwfseqlem4  10086  seqf1olem1  13412  bitsinv2  15794  bitsf1  15797  sadasslem  15821  sadeq  15823  bitsuz  15825  eulerthlem2  16121  f1ocpbllem  16799  f1ovscpbl  16801  fthi  17190  ghmf1  18389  f1omvdmvd  18573  odf1  18691  dprdf1o  19156  ply1scln0  20461  zntoslem  20705  iporthcom  20781  cnt0  21956  cnhaus  21964  imasdsf1olem  22985  imasf1oxmet  22987  dyadmbl  24203  vitalilem3  24213  dvcnvlem  24575  facth1  24760  usgredg2v  27011  cycpmco2lem6  30775  erdszelem9  32448  cvmliftmolem1  32530  msubff1  32805  metf1o  35032  rngoisocnv  35261  laut11  37224  gicabl  39706  fourierdlem50  42448