Theorem eqfnfv 6891

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 6810	. . 3 ⊢ (𝐹 Fn 𝐴 ↔ 𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)))
2		dffn5 6810	. . 3 ⊢ (𝐺 Fn 𝐴 ↔ 𝐺 = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥)))
3		eqeq12 2755	. . 3 ⊢ ((𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) ∧ 𝐺 = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥))) → (𝐹 = 𝐺 ↔ (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥))))
4	1, 2, 3	syl2anb 597	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) → (𝐹 = 𝐺 ↔ (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥))))
5		fvex 6769	. . . 4 ⊢ (𝐹‘𝑥) ∈ V
6	5	rgenw 3075	. . 3 ⊢ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ V
7		mpteqb 6876	. . 3 ⊢ (∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ V → ((𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥)) ↔ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = (𝐺‘𝑥)))
8	6, 7	ax-mp 5	. 2 ⊢ ((𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥)) ↔ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = (𝐺‘𝑥))
9	4, 8	bitrdi 286	1 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) → (𝐹 = 𝐺 ↔ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = (𝐺‘𝑥)))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 395   = wceq 1539   ∈ wcel 2108  ∀wral 3063  Vcvv 3422   ↦ cmpt 5153   Fn wfn 6413  ‘cfv 6418

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pr 5347

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ne 2943  df-ral 3068  df-rex 3069  df-rab 3072  df-v 3424  df-sbc 3712  df-csb 3829  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-opab 5133  df-mpt 5154  df-id 5480  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-res 5592  df-ima 5593  df-iota 6376  df-fun 6420  df-fn 6421  df-fv 6426

This theorem is referenced by:  eqfnfv2  6892  eqfnfvd  6894  eqfnfv2f  6895  fvreseq0  6897  fnmptfvd  6900  fndmdifeq0  6903  fneqeql  6905  fnnfpeq0  7032  fprb  7051  fconst2g  7060  cocan1  7143  cocan2  7144  weniso  7205  fsplitfpar  7930  fnsuppres  7978  tfr3  8201  ixpfi2  9047  fipreima  9055  updjud  9623  fseqenlem1  9711  fpwwe2lem7  10324  ofsubeq0  11900  ser0f  13704  hashgval2  14021  hashf1lem1  14096  hashf1lem1OLD  14097  prodf1f  15532  efcvgfsum  15723  prmreclem2  16546  1arithlem4  16555  1arith  16556  smndex1n0mnd  18466  isgrpinv  18547  dprdf11  19541  frlmplusgvalb  20886  frlmvscavalb  20887  islindf4  20955  psrbagconf1o  21049  psrbagconf1oOLD  21050  pthaus  22697  xkohaus  22712  cnmpt11  22722  cnmpt21  22730  prdsxmetlem  23429  rrxmet  24477  rolle  25059  tdeglem4  25129  tdeglem4OLD  25130  resinf1o  25597  dchrelbas2  26290  dchreq  26311  eqeefv  27174  axlowdimlem14  27226  elntg2  27256  nmlno0lem  29056  phoeqi  29120  occllem  29566  dfiop2  30016  hoeq  30023  ho01i  30091  hoeq1  30093  kbpj  30219  nmlnop0iALT  30258  lnopco0i  30267  nlelchi  30324  rnbra  30370  kbass5  30383  hmopidmchi  30414  hmopidmpji  30415  pjssdif2i  30437  pjinvari  30454  bnj1542  32737  bnj580  32793  subfacp1lem3  33044  subfacp1lem5  33046  mrsubff1  33376  msubff1  33418  faclimlem1  33615  rdgprc  33676  broucube  35738  cocanfo  35803  eqfnun  35807  sdclem2  35827  rrnmet  35914  rrnequiv  35920  ltrnid  38076  ltrneq2  38089  tendoeq1  38705  sticksstones1  40030  pw2f1ocnv  40775  caofcan  41830  addrcom  41982  fsneq  42635  dvnprodlem1  43377  cfsetsnfsetf1  44440  cfsetsnfsetfo  44441  rrx2pnecoorneor  45949  rrx2linest  45976