Theorem eqfnfv 7051

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 6967	. . 3 ⊢ (𝐹 Fn 𝐴 ↔ 𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)))
2		dffn5 6967	. . 3 ⊢ (𝐺 Fn 𝐴 ↔ 𝐺 = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥)))
3		eqeq12 2754	. . 3 ⊢ ((𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) ∧ 𝐺 = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥))) → (𝐹 = 𝐺 ↔ (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥))))
4	1, 2, 3	syl2anb 598	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) → (𝐹 = 𝐺 ↔ (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥))))
5		fvex 6919	. . . 4 ⊢ (𝐹‘𝑥) ∈ V
6	5	rgenw 3065	. . 3 ⊢ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ V
7		mpteqb 7035	. . 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 1540   ∈ wcel 2108  ∀wral 3061  Vcvv 3480   ↦ cmpt 5225   Fn wfn 6556  ‘cfv 6561

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-br 5144  df-opab 5206  df-mpt 5226  df-id 5578  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-iota 6514  df-fun 6563  df-fn 6564  df-fv 6569

This theorem is referenced by:  eqfnfv2  7052  eqfnfvd  7054  eqfnfv2f  7055  eqfnun  7057  fvreseq0  7058  fnmptfvd  7061  fndmdifeq0  7064  fneqeql  7066  fnnfpeq0  7198  fprb  7214  fconst2g  7223  cocan1  7311  cocan2  7312  weniso  7374  fsplitfpar  8143  fnsuppres  8216  tfr3  8439  ixpfi2  9390  fipreima  9398  updjud  9974  fseqenlem1  10064  fpwwe2lem7  10677  ofsubeq0  12263  ser0f  14096  hashgval2  14417  hashf1lem1  14494  prodf1f  15928  efcvgfsum  16122  prmreclem2  16955  1arithlem4  16964  1arith  16965  smndex1n0mnd  18925  isgrpinv  19011  dprdf11  20043  frlmplusgvalb  21789  frlmvscavalb  21790  islindf4  21858  psrbagconf1o  21949  pthaus  23646  xkohaus  23661  cnmpt11  23671  cnmpt21  23679  prdsxmetlem  24378  rrxmet  25442  rolle  26028  tdeglem4  26099  resinf1o  26578  dchrelbas2  27281  dchreq  27302  eqeefv  28918  axlowdimlem14  28970  elntg2  29000  nmlno0lem  30812  phoeqi  30876  occllem  31322  dfiop2  31772  hoeq  31779  ho01i  31847  hoeq1  31849  kbpj  31975  nmlnop0iALT  32014  lnopco0i  32023  nlelchi  32080  rnbra  32126  kbass5  32139  hmopidmchi  32170  hmopidmpji  32171  pjssdif2i  32193  pjinvari  32210  bnj1542  34871  bnj580  34927  subfacp1lem3  35187  subfacp1lem5  35189  mrsubff1  35519  msubff1  35561  faclimlem1  35743  rdgprc  35795  broucube  37661  cocanfo  37726  sdclem2  37749  rrnmet  37836  rrnequiv  37842  ltrnid  40137  ltrneq2  40150  tendoeq1  40766  sticksstones1  42147  pw2f1ocnv  43049  caofcan  44342  addrcom  44494  fsneq  45211  dvnprodlem1  45961  cfsetsnfsetf1  47071  cfsetsnfsetfo  47072  rrx2pnecoorneor  48636  rrx2linest  48663