Theorem eqfnfv 6964

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 6880	. . 3 ⊢ (𝐹 Fn 𝐴 ↔ 𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)))
2		dffn5 6880	. . 3 ⊢ (𝐺 Fn 𝐴 ↔ 𝐺 = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥)))
3		eqeq12 2748	. . 3 ⊢ ((𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) ∧ 𝐺 = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥))) → (𝐹 = 𝐺 ↔ (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥))))
4	1, 2, 3	syl2anb 598	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) → (𝐹 = 𝐺 ↔ (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥))))
5		fvex 6835	. . . 4 ⊢ (𝐹‘𝑥) ∈ V
6	5	rgenw 3051	. . 3 ⊢ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ V
7		mpteqb 6948	. . 3 ⊢ (∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ V → ((𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥)) ↔ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = (𝐺‘𝑥)))
8	6, 7	ax-mp 5	. 2 ⊢ ((𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥)) ↔ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = (𝐺‘𝑥))
9	4, 8	bitrdi 287	1 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) → (𝐹 = 𝐺 ↔ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = (𝐺‘𝑥)))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1541   ∈ wcel 2111  ∀wral 3047  Vcvv 3436   ↦ cmpt 5170   Fn wfn 6476  ‘cfv 6481

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 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-sep 5232  ax-nul 5242  ax-pr 5368

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ne 2929  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-sbc 3737  df-csb 3846  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-nul 4281  df-if 4473  df-sn 4574  df-pr 4576  df-op 4580  df-uni 4857  df-br 5090  df-opab 5152  df-mpt 5171  df-id 5509  df-xp 5620  df-rel 5621  df-cnv 5622  df-co 5623  df-dm 5624  df-rn 5625  df-res 5626  df-ima 5627  df-iota 6437  df-fun 6483  df-fn 6484  df-fv 6489

This theorem is referenced by:  eqfnfv2  6965  eqfnfvd  6967  eqfnfv2f  6968  eqfnun  6970  fvreseq0  6971  fnmptfvd  6974  fndmdifeq0  6977  fneqeql  6979  fnnfpeq0  7112  fprb  7128  fconst2g  7137  cocan1  7225  cocan2  7226  weniso  7288  fsplitfpar  8048  fnsuppres  8121  tfr3  8318  ixpfi2  9234  fipreima  9242  updjud  9827  fseqenlem1  9915  fpwwe2lem7  10528  ofsubeq0  12122  ser0f  13962  hashgval2  14285  hashf1lem1  14362  prodf1f  15799  efcvgfsum  15993  prmreclem2  16829  1arithlem4  16838  1arith  16839  smndex1n0mnd  18820  isgrpinv  18906  dprdf11  19937  frlmplusgvalb  21706  frlmvscavalb  21707  islindf4  21775  psrbagconf1o  21866  pthaus  23553  xkohaus  23568  cnmpt11  23578  cnmpt21  23586  prdsxmetlem  24283  rrxmet  25335  rolle  25921  tdeglem4  25992  resinf1o  26472  dchrelbas2  27175  dchreq  27196  eqeefv  28881  axlowdimlem14  28933  elntg2  28963  nmlno0lem  30773  phoeqi  30837  occllem  31283  dfiop2  31733  hoeq  31740  ho01i  31808  hoeq1  31810  kbpj  31936  nmlnop0iALT  31975  lnopco0i  31984  nlelchi  32041  rnbra  32087  kbass5  32100  hmopidmchi  32131  hmopidmpji  32132  pjssdif2i  32154  pjinvari  32171  bnj1542  34869  bnj580  34925  subfacp1lem3  35226  subfacp1lem5  35228  mrsubff1  35558  msubff1  35600  faclimlem1  35787  rdgprc  35836  broucube  37704  cocanfo  37769  sdclem2  37792  rrnmet  37879  rrnequiv  37885  ltrnid  40244  ltrneq2  40257  tendoeq1  40873  sticksstones1  42249  pw2f1ocnv  43140  caofcan  44426  addrcom  44577  fsneq  45313  dvnprodlem1  46054  cfsetsnfsetf1  47169  cfsetsnfsetfo  47170  rrx2pnecoorneor  48826  rrx2linest  48853  dfinito4  49612