Theorem eqfnfv 6971

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 6885	. . 3 ⊢ (𝐹 Fn 𝐴 ↔ 𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)))
2		dffn5 6885	. . 3 ⊢ (𝐺 Fn 𝐴 ↔ 𝐺 = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥)))
3		eqeq12 2756	. . 3 ⊢ ((𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) ∧ 𝐺 = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥))) → (𝐹 = 𝐺 ↔ (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥))))
4	1, 2, 3	syl2anb 604	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) → (𝐹 = 𝐺 ↔ (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥))))
5		fvex 6840	. . . 4 ⊢ (𝐹‘𝑥) ∈ V
6	5	rgenw 3057	. . 3 ⊢ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ V
7		mpteqb 6955	. . 3 ⊢ (∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ V → ((𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥)) ↔ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = (𝐺‘𝑥)))
8	6, 7	ax-mp 5	. 2 ⊢ ((𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥)) ↔ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = (𝐺‘𝑥))
9	4, 8	bitrdi 288	1 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) → (𝐹 = 𝐺 ↔ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = (𝐺‘𝑥)))

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396   = wceq 1547   ∈ wcel 2119  ∀wral 3053  Vcvv 3431   ↦ cmpt 5153   Fn wfn 6480  ‘cfv 6485

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2711  ax-sep 5218  ax-nul 5228  ax-pr 5362

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2718  df-cleq 2731  df-clel 2814  df-nfc 2888  df-ne 2935  df-ral 3054  df-rex 3064  df-rab 3392  df-v 3433  df-sbc 3724  df-csb 3832  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4262  df-if 4455  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-br 5073  df-opab 5135  df-mpt 5154  df-id 5513  df-xp 5624  df-rel 5625  df-cnv 5626  df-co 5627  df-dm 5628  df-rn 5629  df-res 5630  df-ima 5631  df-iota 6441  df-fun 6487  df-fn 6488  df-fv 6493

This theorem is referenced by:  eqfnfv2  6972  eqfnfvd  6974  eqfnfv2f  6975  fsneq  6976  eqfnun  6978  fvreseq0  6979  fnmptfvd  6982  fndmdifeq0  6985  fneqeql  6987  fnnfpeq0  7122  fprb  7138  fconst2g  7147  cocan1  7235  cocan2  7236  weniso  7298  fsplitfpar  8057  fnsuppres  8131  tfr3  8328  ixpfi2  9250  fipreima  9258  updjud  9849  fseqenlem1  9937  fpwwe2lem7  10551  ofsubeq0  12147  ser0f  14008  hashgval2  14331  hashf1lem1  14408  prodf1f  15848  efcvgfsum  16042  prmreclem2  16879  1arithlem4  16888  1arith  16889  smndex1n0mnd  18874  isgrpinv  18960  dprdf11  19991  frlmplusgvalb  21744  frlmvscavalb  21745  islindf4  21813  psrbagconf1o  21904  pthaus  23621  xkohaus  23636  cnmpt11  23646  cnmpt21  23654  prdsxmetlem  24351  rrxmet  25393  rolle  25975  tdeglem4  26043  resinf1o  26518  dchrelbas2  27218  dchreq  27239  eqeefv  28990  axlowdimlem14  29042  elntg2  29072  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  35039  bnj580  35095  subfacp1lem3  35410  subfacp1lem5  35412  mrsubff1  35742  msubff1  35784  faclimlem1  35971  rdgprc  36020  broucube  38021  cocanfo  38086  sdclem2  38109  rrnmet  38196  rrnequiv  38202  ltrnid  40627  ltrneq2  40640  tendoeq1  41256  sticksstones1  42631  pw2f1ocnv  43482  caofcan  44767  addrcom  44918  dvnprodlem1  46389  cfsetsnfsetf1  47522  cfsetsnfsetfo  47523  rrx2pnecoorneor  49206  rrx2linest  49233  dfinito4  49991