Theorem f1fveq 7265

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1570   ∈ wcel 2146  –1-1→wf1 6537  ‘cfv 6540

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737  ax-sep 5259  ax-nul 5271  ax-pr 5406

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-ne 2961  df-ral 3082  df-rex 3092  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-opab 5176  df-id 5558  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-iota 6496  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fv 6548

This theorem is used by:  f1elima  7266  f1dom3fv3dif  7271  cocan1  7298  isof1oidb  7331  isosolem  7354  f1oiso  7358  weniso  7363  f1oweALT  7975  2dom  9034  xpdom2  9067  wemapwe  9673  fseqenlem1  10024  dfac12lem2  10144  infpssrlem4  10305  fin23lem28  10339  isf32lem7  10358  iundom2g  10539  canthnumlem  10648  canthwelem  10650  canthp1lem2  10653  pwfseqlem4  10662  seqf1olem1  14095  bitsinv2  16523  bitsf1  16526  sadasslem  16550  sadeq  16552  bitsuz  16554  eulerthlem2  16863  f1ocpbllem  17600  f1ovscpbl  17602  fthi  17999  f1omvdmvd  19557  odf1  19676  dprdf1o  20148  zntoslem  21756  iporthcom  21835  ply1scln0  22502  cnt0  23553  cnhaus  23561  imasdsf1olem  24581  imasf1oxmet  24583  dyadmbl  25810  vitalilem3  25820  dvcnvlem  26186  facth1  26375  usgredg2v  29635  mndlactf1o  33414  mndractf1o  33415  cycpmco2lem6  33515  erdszelem9  35728  cvmliftmolem1  35810  msubff1  36085  metf1o  38464  rngoisocnv  38690  laut11  40918  aks6d1c6lem3  42997  gicabl  43884  permac8prim  45781  fourierdlem50  46928  isuspgrim0lem  48716  uptrlem1  50045