Theorem eqfnfv 7023

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 6937	. . 3 ⊢ (𝐹 Fn 𝐴 ↔ 𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)))
2		dffn5 6937	. . 3 ⊢ (𝐺 Fn 𝐴 ↔ 𝐺 = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥)))
3		eqeq12 2777	. . 3 ⊢ ((𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) ∧ 𝐺 = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥))) → (𝐹 = 𝐺 ↔ (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥))))
4	1, 2, 3	syl2anb 610	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) → (𝐹 = 𝐺 ↔ (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥))))
5		fvex 6892	. . . 4 ⊢ (𝐹‘𝑥) ∈ V
6	5	rgenw 3080	. . 3 ⊢ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ V
7		mpteqb 7007	. . 3 ⊢ (∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ V → ((𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥)) ↔ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = (𝐺‘𝑥)))
8	6, 7	ax-mp 5	. 2 ⊢ ((𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥)) ↔ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = (𝐺‘𝑥))
9	4, 8	bitrdi 290	1 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) → (𝐹 = 𝐺 ↔ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = (𝐺‘𝑥)))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1570   ∈ wcel 2145  ∀wral 3076  Vcvv 3450   ↦ cmpt 5186   Fn wfn 6528  ‘cfv 6533

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 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-sep 5251  ax-nul 5263  ax-pr 5398

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 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-mpt 5187  df-id 5550  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-iota 6489  df-fun 6535  df-fn 6536  df-fv 6541

This theorem is used by:  eqfnfv2  7024  eqfnfvd  7026  eqfnfv2f  7027  fsneq  7028  eqfnun  7030  fvreseq0  7031  fnmptfvd  7034  fndmdifeq0  7037  fneqeql  7039  fnnfpeq0  7177  fprb  7193  fconst2g  7203  cocan1  7293  cocan2  7294  weniso  7358  fsplitfpar  8116  fnsuppres  8190  tfr3  8389  ixpfi2  9320  fipreima  9328  updjud  9942  fseqenlem1  10030  fpwwe2lem7  10649  ofsubeq0  12242  ser0f  14122  hashgval2  14445  hashf1lem1  14523  prodf1f  15984  efcvgfsum  16175  prmreclem2  17012  1arithlem4  17021  1arith  17022  smndex1n0mnd  19027  isgrpinv  19120  dprdf11  20155  frlmplusgvalb  21985  frlmvscavalb  21986  islindf4  22054  psrbagconf1o  22147  pthaus  23867  xkohaus  23882  cnmpt11  23892  cnmpt21  23900  prdsxmetlem  24597  rrxmet  25639  rolle  26220  tdeglem4  26288  resinf1o  26776  dchrelbas2  27476  dchreq  27497  eqeefv  29363  axlowdimlem14  29415  elntg2  29445  nmlno0lem  31277  phoeqi  31341  occllem  31787  dfiop2  32237  hoeq  32244  ho01i  32312  hoeq1  32314  kbpj  32440  nmlnop0iALT  32479  lnopco0i  32488  nlelchi  32545  rnbra  32591  kbass5  32604  hmopidmchi  32635  hmopidmpji  32636  pjssdif2i  32658  pjinvari  32675  bnj1542  35369  bnj580  35425  subfacp1lem3  35764  subfacp1lem5  35766  mrsubff1  36096  msubff1  36138  faclimlem1  36325  rdgprc  36374  broucube  38406  cocanfo  38472  sdclem2  38495  rrnmet  38582  rrnequiv  38588  ltrnid  41011  ltrneq2  41024  tendoeq1  41640  sticksstones1  43015  pw2f1ocnv  43881  caofcan  45150  addrcom  45300  dvnprodlem1  46777  cfsetsnfsetf1  47950  cfsetsnfsetfo  47951  rrx2pnecoorneor  49648  rrx2linest  49675  dfinito4  50430