Theorem eqfnfv 6978

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 6893	. . 3 ⊢ (𝐹 Fn 𝐴 ↔ 𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)))
2		dffn5 6893	. . 3 ⊢ (𝐺 Fn 𝐴 ↔ 𝐺 = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥)))
3		eqeq12 2754	. . 3 ⊢ ((𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) ∧ 𝐺 = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥))) → (𝐹 = 𝐺 ↔ (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥))))
4	1, 2, 3	syl2anb 599	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) → (𝐹 = 𝐺 ↔ (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥))))
5		fvex 6848	. . . 4 ⊢ (𝐹‘𝑥) ∈ V
6	5	rgenw 3056	. . 3 ⊢ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ V
7		mpteqb 6962	. . 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 6488  ‘cfv 6493

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 5232  ax-nul 5242  ax-pr 5371

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 5520  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-iota 6449  df-fun 6495  df-fn 6496  df-fv 6501

This theorem is referenced by:  eqfnfv2  6979  eqfnfvd  6981  eqfnfv2f  6982  eqfnun  6984  fvreseq0  6985  fnmptfvd  6988  fndmdifeq0  6991  fneqeql  6993  fnnfpeq0  7127  fprb  7143  fconst2g  7152  cocan1  7240  cocan2  7241  weniso  7303  fsplitfpar  8062  fnsuppres  8135  tfr3  8332  ixpfi2  9254  fipreima  9262  updjud  9852  fseqenlem1  9940  fpwwe2lem7  10554  ofsubeq0  12150  ser0f  14011  hashgval2  14334  hashf1lem1  14411  prodf1f  15851  efcvgfsum  16045  prmreclem2  16882  1arithlem4  16891  1arith  16892  smndex1n0mnd  18877  isgrpinv  18963  dprdf11  19994  frlmplusgvalb  21762  frlmvscavalb  21763  islindf4  21831  psrbagconf1o  21922  pthaus  23616  xkohaus  23631  cnmpt11  23641  cnmpt21  23649  prdsxmetlem  24346  rrxmet  25388  rolle  25970  tdeglem4  26038  resinf1o  26516  dchrelbas2  27217  dchreq  27238  eqeefv  28989  axlowdimlem14  29041  elntg2  29071  nmlno0lem  30882  phoeqi  30946  occllem  31392  dfiop2  31842  hoeq  31849  ho01i  31917  hoeq1  31919  kbpj  32045  nmlnop0iALT  32084  lnopco0i  32093  nlelchi  32150  rnbra  32196  kbass5  32209  hmopidmchi  32240  hmopidmpji  32241  pjssdif2i  32263  pjinvari  32280  bnj1542  35018  bnj580  35074  subfacp1lem3  35383  subfacp1lem5  35385  mrsubff1  35715  msubff1  35757  faclimlem1  35944  rdgprc  35993  broucube  37992  cocanfo  38057  sdclem2  38080  rrnmet  38167  rrnequiv  38173  ltrnid  40598  ltrneq2  40611  tendoeq1  41227  sticksstones1  42602  pw2f1ocnv  43486  caofcan  44771  addrcom  44922  fsneq  45656  dvnprodlem1  46395  cfsetsnfsetf1  47522  cfsetsnfsetfo  47523  rrx2pnecoorneor  49206  rrx2linest  49233  dfinito4  49991