Theorem eqfnfv 6983

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 6898	. . 3 ⊢ (𝐹 Fn 𝐴 ↔ 𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)))
2		dffn5 6898	. . 3 ⊢ (𝐺 Fn 𝐴 ↔ 𝐺 = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥)))
3		eqeq12 2753	. . 3 ⊢ ((𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) ∧ 𝐺 = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥))) → (𝐹 = 𝐺 ↔ (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥))))
4	1, 2, 3	syl2anb 599	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) → (𝐹 = 𝐺 ↔ (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥))))
5		fvex 6853	. . . 4 ⊢ (𝐹‘𝑥) ∈ V
6	5	rgenw 3055	. . 3 ⊢ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ V
7		mpteqb 6967	. . 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 1542   ∈ wcel 2114  ∀wral 3051  Vcvv 3429   ↦ cmpt 5166   Fn wfn 6493  ‘cfv 6498

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2708  ax-sep 5231  ax-nul 5241  ax-pr 5375

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3062  df-rab 3390  df-v 3431  df-sbc 3729  df-csb 3838  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-br 5086  df-opab 5148  df-mpt 5167  df-id 5526  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-iota 6454  df-fun 6500  df-fn 6501  df-fv 6506

This theorem is referenced by:  eqfnfv2  6984  eqfnfvd  6986  eqfnfv2f  6987  eqfnun  6989  fvreseq0  6990  fnmptfvd  6993  fndmdifeq0  6996  fneqeql  6998  fnnfpeq0  7133  fprb  7149  fconst2g  7158  cocan1  7246  cocan2  7247  weniso  7309  fsplitfpar  8068  fnsuppres  8141  tfr3  8338  ixpfi2  9260  fipreima  9268  updjud  9858  fseqenlem1  9946  fpwwe2lem7  10560  ofsubeq0  12156  ser0f  14017  hashgval2  14340  hashf1lem1  14417  prodf1f  15857  efcvgfsum  16051  prmreclem2  16888  1arithlem4  16897  1arith  16898  smndex1n0mnd  18883  isgrpinv  18969  dprdf11  20000  frlmplusgvalb  21749  frlmvscavalb  21750  islindf4  21818  psrbagconf1o  21909  pthaus  23603  xkohaus  23618  cnmpt11  23628  cnmpt21  23636  prdsxmetlem  24333  rrxmet  25375  rolle  25957  tdeglem4  26025  resinf1o  26500  dchrelbas2  27200  dchreq  27221  eqeefv  28972  axlowdimlem14  29024  elntg2  29054  nmlno0lem  30864  phoeqi  30928  occllem  31374  dfiop2  31824  hoeq  31831  ho01i  31899  hoeq1  31901  kbpj  32027  nmlnop0iALT  32066  lnopco0i  32075  nlelchi  32132  rnbra  32178  kbass5  32191  hmopidmchi  32222  hmopidmpji  32223  pjssdif2i  32245  pjinvari  32262  bnj1542  34999  bnj580  35055  subfacp1lem3  35364  subfacp1lem5  35366  mrsubff1  35696  msubff1  35738  faclimlem1  35925  rdgprc  35974  broucube  37975  cocanfo  38040  sdclem2  38063  rrnmet  38150  rrnequiv  38156  ltrnid  40581  ltrneq2  40594  tendoeq1  41210  sticksstones1  42585  pw2f1ocnv  43465  caofcan  44750  addrcom  44901  fsneq  45635  dvnprodlem1  46374  cfsetsnfsetf1  47507  cfsetsnfsetfo  47508  rrx2pnecoorneor  49191  rrx2linest  49218  dfinito4  49976