Theorem eqfnfv 6779

Description: Equality of functions is determined by their values. Special case of Exercise 4 of [TakeutiZaring] p. 28 (with domain equality omitted). (Contributed by NM, 3-Aug-1994.) (Proof shortened by Andrew Salmon, 22-Oct-2011.) (Proof shortened by Mario Carneiro, 31-Aug-2015.)

Assertion

Ref	Expression
eqfnfv	⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) → (𝐹 = 𝐺 ↔ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = (𝐺‘𝑥)))

Distinct variable groups:   𝑥,𝐴   𝑥,𝐹   𝑥,𝐺

Proof of Theorem eqfnfv

Step	Hyp	Ref	Expression
1		dffn5 6699	. . 3 ⊢ (𝐹 Fn 𝐴 ↔ 𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)))
2		dffn5 6699	. . 3 ⊢ (𝐺 Fn 𝐴 ↔ 𝐺 = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥)))
3		eqeq12 2812	. . 3 ⊢ ((𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) ∧ 𝐺 = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥))) → (𝐹 = 𝐺 ↔ (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥))))
4	1, 2, 3	syl2anb 600	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) → (𝐹 = 𝐺 ↔ (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥))))
5		fvex 6658	. . . 4 ⊢ (𝐹‘𝑥) ∈ V
6	5	rgenw 3118	. . 3 ⊢ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ V
7		mpteqb 6764	. . 3 ⊢ (∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ V → ((𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥)) ↔ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = (𝐺‘𝑥)))
8	6, 7	ax-mp 5	. 2 ⊢ ((𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥)) ↔ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = (𝐺‘𝑥))
9	4, 8	syl6bb 290	1 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) → (𝐹 = 𝐺 ↔ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = (𝐺‘𝑥)))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1538   ∈ wcel 2111  ∀wral 3106  Vcvv 3441   ↦ cmpt 5110   Fn wfn 6319  ‘cfv 6324

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5167  ax-nul 5174  ax-pow 5231  ax-pr 5295

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ral 3111  df-rex 3112  df-rab 3115  df-v 3443  df-sbc 3721  df-csb 3829  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-nul 4244  df-if 4426  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4801  df-br 5031  df-opab 5093  df-mpt 5111  df-id 5425  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532  df-iota 6283  df-fun 6326  df-fn 6327  df-fv 6332

This theorem is referenced by:  eqfnfv2  6780  eqfnfvd  6782  eqfnfv2f  6783  fvreseq0  6785  fnmptfvd  6788  fndmdifeq0  6791  fneqeql  6793  fnnfpeq0  6917  fprb  6933  fconst2g  6942  cocan1  7025  cocan2  7026  weniso  7086  fsplitfpar  7797  fnsuppres  7840  tfr3  8018  ixpfi2  8806  fipreima  8814  updjud  9347  fseqenlem1  9435  fpwwe2lem8  10048  ofsubeq0  11622  ser0f  13419  hashgval2  13735  hashf1lem1  13809  prodf1f  15240  efcvgfsum  15431  prmreclem2  16243  1arithlem4  16252  1arith  16253  smndex1n0mnd  18069  isgrpinv  18148  dprdf11  19138  frlmplusgvalb  20458  frlmvscavalb  20459  islindf4  20527  psrbagconf1o  20612  pthaus  22243  xkohaus  22258  cnmpt11  22268  cnmpt21  22276  prdsxmetlem  22975  rrxmet  24012  rolle  24593  tdeglem4  24661  resinf1o  25128  dchrelbas2  25821  dchreq  25842  eqeefv  26697  axlowdimlem14  26749  elntg2  26779  nmlno0lem  28576  phoeqi  28640  occllem  29086  dfiop2  29536  hoeq  29543  ho01i  29611  hoeq1  29613  kbpj  29739  nmlnop0iALT  29778  lnopco0i  29787  nlelchi  29844  rnbra  29890  kbass5  29903  hmopidmchi  29934  hmopidmpji  29935  pjssdif2i  29957  pjinvari  29974  bnj1542  32239  bnj580  32295  subfacp1lem3  32542  subfacp1lem5  32544  mrsubff1  32874  msubff1  32916  faclimlem1  33088  rdgprc  33152  broucube  35091  cocanfo  35156  eqfnun  35160  sdclem2  35180  rrnmet  35267  rrnequiv  35273  ltrnid  37431  ltrneq2  37444  tendoeq1  38060  pw2f1ocnv  39978  caofcan  41027  addrcom  41179  fsneq  41835  dvnprodlem1  42588  rrx2pnecoorneor  45129  rrx2linest  45156