Theorem eqfnfv 6796

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 6718	. . 3 ⊢ (𝐹 Fn 𝐴 ↔ 𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)))
2		dffn5 6718	. . 3 ⊢ (𝐺 Fn 𝐴 ↔ 𝐺 = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥)))
3		eqeq12 2835	. . 3 ⊢ ((𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) ∧ 𝐺 = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥))) → (𝐹 = 𝐺 ↔ (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥))))
4	1, 2, 3	syl2anb 599	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) → (𝐹 = 𝐺 ↔ (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥))))
5		fvex 6677	. . . 4 ⊢ (𝐹‘𝑥) ∈ V
6	5	rgenw 3150	. . 3 ⊢ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ V
7		mpteqb 6781	. . 3 ⊢ (∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ V → ((𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥)) ↔ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = (𝐺‘𝑥)))
8	6, 7	ax-mp 5	. 2 ⊢ ((𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥)) ↔ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = (𝐺‘𝑥))
9	4, 8	syl6bb 289	1 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) → (𝐹 = 𝐺 ↔ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = (𝐺‘𝑥)))

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398   = wceq 1533   ∈ wcel 2110  ∀wral 3138  Vcvv 3494   ↦ cmpt 5138   Fn wfn 6344  ‘cfv 6349

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793  ax-sep 5195  ax-nul 5202  ax-pow 5258  ax-pr 5321

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3496  df-sbc 3772  df-csb 3883  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-nul 4291  df-if 4467  df-sn 4561  df-pr 4563  df-op 4567  df-uni 4832  df-br 5059  df-opab 5121  df-mpt 5139  df-id 5454  df-xp 5555  df-rel 5556  df-cnv 5557  df-co 5558  df-dm 5559  df-rn 5560  df-res 5561  df-ima 5562  df-iota 6308  df-fun 6351  df-fn 6352  df-fv 6357

This theorem is referenced by:  eqfnfv2  6797  eqfnfvd  6799  eqfnfv2f  6800  fvreseq0  6802  fnmptfvd  6805  fndmdifeq0  6808  fneqeql  6810  fnnfpeq0  6934  fprb  6950  fconst2g  6959  cocan1  7041  cocan2  7042  weniso  7101  fsplitfpar  7808  fnsuppres  7851  tfr3  8029  ixpfi2  8816  fipreima  8824  updjud  9357  fseqenlem1  9444  fpwwe2lem8  10053  ofsubeq0  11629  ser0f  13417  hashgval2  13733  hashf1lem1  13807  prodf1f  15242  efcvgfsum  15433  prmreclem2  16247  1arithlem4  16256  1arith  16257  smndex1n0mnd  18071  isgrpinv  18150  dprdf11  19139  psrbagconf1o  20148  frlmplusgvalb  20907  frlmvscavalb  20908  islindf4  20976  pthaus  22240  xkohaus  22255  cnmpt11  22265  cnmpt21  22273  prdsxmetlem  22972  rrxmet  24005  rolle  24581  tdeglem4  24648  resinf1o  25114  dchrelbas2  25807  dchreq  25828  eqeefv  26683  axlowdimlem14  26735  elntg2  26765  nmlno0lem  28564  phoeqi  28628  occllem  29074  dfiop2  29524  hoeq  29531  ho01i  29599  hoeq1  29601  kbpj  29727  nmlnop0iALT  29766  lnopco0i  29775  nlelchi  29832  rnbra  29878  kbass5  29891  hmopidmchi  29922  hmopidmpji  29923  pjssdif2i  29945  pjinvari  29962  bnj1542  32124  bnj580  32180  subfacp1lem3  32424  subfacp1lem5  32426  mrsubff1  32756  msubff1  32798  faclimlem1  32970  rdgprc  33034  broucube  34920  cocanfo  34987  eqfnun  34991  sdclem2  35011  rrnmet  35101  rrnequiv  35107  ltrnid  37265  ltrneq2  37278  tendoeq1  37894  pw2f1ocnv  39627  caofcan  40648  addrcom  40800  fsneq  41462  dvnprodlem1  42224  rrx2pnecoorneor  44696  rrx2linest  44723