Theorem eqfnfv 6975

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 6890	. . 3 ⊢ (𝐹 Fn 𝐴 ↔ 𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)))
2		dffn5 6890	. . 3 ⊢ (𝐺 Fn 𝐴 ↔ 𝐺 = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥)))
3		eqeq12 2754	. . 3 ⊢ ((𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) ∧ 𝐺 = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥))) → (𝐹 = 𝐺 ↔ (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥))))
4	1, 2, 3	syl2anb 599	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) → (𝐹 = 𝐺 ↔ (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥))))
5		fvex 6845	. . . 4 ⊢ (𝐹‘𝑥) ∈ V
6	5	rgenw 3056	. . 3 ⊢ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ V
7		mpteqb 6959	. . 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 3052  Vcvv 3430   ↦ cmpt 5167   Fn wfn 6485  ‘cfv 6490

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 2709  ax-sep 5231  ax-nul 5241  ax-pr 5368

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 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5517  df-xp 5628  df-rel 5629  df-cnv 5630  df-co 5631  df-dm 5632  df-rn 5633  df-res 5634  df-ima 5635  df-iota 6446  df-fun 6492  df-fn 6493  df-fv 6498

This theorem is referenced by:  eqfnfv2  6976  eqfnfvd  6978  eqfnfv2f  6979  eqfnun  6981  fvreseq0  6982  fnmptfvd  6985  fndmdifeq0  6988  fneqeql  6990  fnnfpeq0  7124  fprb  7140  fconst2g  7149  cocan1  7237  cocan2  7238  weniso  7300  fsplitfpar  8059  fnsuppres  8132  tfr3  8329  ixpfi2  9251  fipreima  9259  updjud  9847  fseqenlem1  9935  fpwwe2lem7  10549  ofsubeq0  12145  ser0f  14006  hashgval2  14329  hashf1lem1  14406  prodf1f  15846  efcvgfsum  16040  prmreclem2  16877  1arithlem4  16886  1arith  16887  smndex1n0mnd  18872  isgrpinv  18958  dprdf11  19989  frlmplusgvalb  21757  frlmvscavalb  21758  islindf4  21826  psrbagconf1o  21917  pthaus  23612  xkohaus  23627  cnmpt11  23637  cnmpt21  23645  prdsxmetlem  24342  rrxmet  25384  rolle  25966  tdeglem4  26037  resinf1o  26516  dchrelbas2  27219  dchreq  27240  eqeefv  28991  axlowdimlem14  29043  elntg2  29073  nmlno0lem  30884  phoeqi  30948  occllem  31394  dfiop2  31844  hoeq  31851  ho01i  31919  hoeq1  31921  kbpj  32047  nmlnop0iALT  32086  lnopco0i  32095  nlelchi  32152  rnbra  32198  kbass5  32211  hmopidmchi  32242  hmopidmpji  32243  pjssdif2i  32265  pjinvari  32282  bnj1542  35020  bnj580  35076  subfacp1lem3  35385  subfacp1lem5  35387  mrsubff1  35717  msubff1  35759  faclimlem1  35946  rdgprc  35995  broucube  37986  cocanfo  38051  sdclem2  38074  rrnmet  38161  rrnequiv  38167  ltrnid  40592  ltrneq2  40605  tendoeq1  41221  sticksstones1  42596  pw2f1ocnv  43480  caofcan  44765  addrcom  44916  fsneq  45650  dvnprodlem1  46389  cfsetsnfsetf1  47504  cfsetsnfsetfo  47505  rrx2pnecoorneor  49188  rrx2linest  49215  dfinito4  49973