Theorem eqfnfv 6965

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 6881	. . 3 ⊢ (𝐹 Fn 𝐴 ↔ 𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)))
2		dffn5 6881	. . 3 ⊢ (𝐺 Fn 𝐴 ↔ 𝐺 = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥)))
3		eqeq12 2746	. . 3 ⊢ ((𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) ∧ 𝐺 = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥))) → (𝐹 = 𝐺 ↔ (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥))))
4	1, 2, 3	syl2anb 598	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) → (𝐹 = 𝐺 ↔ (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥))))
5		fvex 6835	. . . 4 ⊢ (𝐹‘𝑥) ∈ V
6	5	rgenw 3048	. . 3 ⊢ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ V
7		mpteqb 6949	. . 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 1540   ∈ wcel 2109  ∀wral 3044  Vcvv 3436   ↦ cmpt 5173   Fn wfn 6477  ‘cfv 6482

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5235  ax-nul 5245  ax-pr 5371

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-rab 3395  df-v 3438  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4859  df-br 5093  df-opab 5155  df-mpt 5174  df-id 5514  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632  df-iota 6438  df-fun 6484  df-fn 6485  df-fv 6490

This theorem is referenced by:  eqfnfv2  6966  eqfnfvd  6968  eqfnfv2f  6969  eqfnun  6971  fvreseq0  6972  fnmptfvd  6975  fndmdifeq0  6978  fneqeql  6980  fnnfpeq0  7114  fprb  7130  fconst2g  7139  cocan1  7228  cocan2  7229  weniso  7291  fsplitfpar  8051  fnsuppres  8124  tfr3  8321  ixpfi2  9240  fipreima  9248  updjud  9830  fseqenlem1  9918  fpwwe2lem7  10531  ofsubeq0  12125  ser0f  13962  hashgval2  14285  hashf1lem1  14362  prodf1f  15799  efcvgfsum  15993  prmreclem2  16829  1arithlem4  16838  1arith  16839  smndex1n0mnd  18786  isgrpinv  18872  dprdf11  19904  frlmplusgvalb  21676  frlmvscavalb  21677  islindf4  21745  psrbagconf1o  21836  pthaus  23523  xkohaus  23538  cnmpt11  23548  cnmpt21  23556  prdsxmetlem  24254  rrxmet  25306  rolle  25892  tdeglem4  25963  resinf1o  26443  dchrelbas2  27146  dchreq  27167  eqeefv  28848  axlowdimlem14  28900  elntg2  28930  nmlno0lem  30737  phoeqi  30801  occllem  31247  dfiop2  31697  hoeq  31704  ho01i  31772  hoeq1  31774  kbpj  31900  nmlnop0iALT  31939  lnopco0i  31948  nlelchi  32005  rnbra  32051  kbass5  32064  hmopidmchi  32095  hmopidmpji  32096  pjssdif2i  32118  pjinvari  32135  bnj1542  34830  bnj580  34886  subfacp1lem3  35165  subfacp1lem5  35167  mrsubff1  35497  msubff1  35539  faclimlem1  35726  rdgprc  35778  broucube  37644  cocanfo  37709  sdclem2  37732  rrnmet  37819  rrnequiv  37825  ltrnid  40124  ltrneq2  40137  tendoeq1  40753  sticksstones1  42129  pw2f1ocnv  43020  caofcan  44306  addrcom  44458  fsneq  45194  dvnprodlem1  45937  cfsetsnfsetf1  47053  cfsetsnfsetfo  47054  rrx2pnecoorneor  48710  rrx2linest  48737  dfinito4  49496