Theorem eqfnfv 6455

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 6384	. . 3 ⊢ (𝐹 Fn 𝐴 ↔ 𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)))
2		dffn5 6384	. . 3 ⊢ (𝐺 Fn 𝐴 ↔ 𝐺 = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥)))
3		eqeq12 2784	. . 3 ⊢ ((𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) ∧ 𝐺 = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥))) → (𝐹 = 𝐺 ↔ (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥))))
4	1, 2, 3	syl2anb 579	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) → (𝐹 = 𝐺 ↔ (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥))))
5		fvex 6343	. . . 4 ⊢ (𝐹‘𝑥) ∈ V
6	5	rgenw 3073	. . 3 ⊢ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ V
7		mpteqb 6442	. . 3 ⊢ (∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ V → ((𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥)) ↔ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = (𝐺‘𝑥)))
8	6, 7	ax-mp 5	. 2 ⊢ ((𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥)) ↔ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = (𝐺‘𝑥))
9	4, 8	syl6bb 276	1 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) → (𝐹 = 𝐺 ↔ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = (𝐺‘𝑥)))

Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 382   = wceq 1631   ∈ wcel 2145  ∀wral 3061  Vcvv 3351   ↦ cmpt 4864   Fn wfn 6027  ‘cfv 6032

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-sep 4916  ax-nul 4924  ax-pow 4975  ax-pr 5035

This theorem depends on definitions:  df-bi 197  df-an 383  df-or 829  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ral 3066  df-rex 3067  df-rab 3070  df-v 3353  df-sbc 3589  df-csb 3684  df-dif 3727  df-un 3729  df-in 3731  df-ss 3738  df-nul 4065  df-if 4227  df-sn 4318  df-pr 4320  df-op 4324  df-uni 4576  df-br 4788  df-opab 4848  df-mpt 4865  df-id 5158  df-xp 5256  df-rel 5257  df-cnv 5258  df-co 5259  df-dm 5260  df-rn 5261  df-res 5262  df-ima 5263  df-iota 5995  df-fun 6034  df-fn 6035  df-fv 6040

This theorem is referenced by:  eqfnfv2  6456  eqfnfvd  6458  eqfnfv2f  6459  fvreseq0  6461  fnmptfvd  6464  fndmdifeq0  6467  fneqeql  6469  fnnfpeq0  6589  fconst2g  6613  cocan1  6690  cocan2  6691  weniso  6748  fnsuppres  7475  tfr3  7649  ixpfi2  8421  fipreima  8429  updjud  8961  fseqenlem1  9048  fpwwe2lem8  9662  ofsubeq0  11220  ser0f  13062  hashgval2  13370  hashf1lem1  13442  prodf1f  14832  efcvgfsum  15023  prmreclem2  15829  1arithlem4  15838  1arith  15839  isgrpinv  17681  dprdf11  18631  psrbagconf1o  19590  islindf4  20395  pthaus  21663  xkohaus  21678  cnmpt11  21688  cnmpt21  21696  prdsxmetlem  22394  rrxmet  23411  rolle  23974  tdeglem4  24041  resinf1o  24504  dchrelbas2  25184  dchreq  25205  eqeefv  26005  axlowdimlem14  26057  nmlno0lem  27989  phoeqi  28054  occllem  28503  dfiop2  28953  hoeq  28960  ho01i  29028  hoeq1  29030  kbpj  29156  nmlnop0iALT  29195  lnopco0i  29204  nlelchi  29261  rnbra  29307  kbass5  29320  hmopidmchi  29351  hmopidmpji  29352  pjssdif2i  29374  pjinvari  29391  bnj1542  31266  bnj580  31322  subfacp1lem3  31503  subfacp1lem5  31505  mrsubff1  31750  msubff1  31792  faclimlem1  31968  fprb  32008  rdgprc  32037  broucube  33777  cocanfo  33845  eqfnun  33849  sdclem2  33871  rrnmet  33961  rrnequiv  33967  ltrnid  35944  ltrneq2  35957  tendoeq1  36574  pw2f1ocnv  38131  caofcan  39049  addrcom  39205  fsneq  39917  dvnprodlem1  40680