Theorem eqfnfv 6462

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 6391	. . 3 ⊢ (𝐹 Fn 𝐴 ↔ 𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)))
2		dffn5 6391	. . 3 ⊢ (𝐺 Fn 𝐴 ↔ 𝐺 = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥)))
3		eqeq12 2761	. . 3 ⊢ ((𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) ∧ 𝐺 = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥))) → (𝐹 = 𝐺 ↔ (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥))))
4	1, 2, 3	syl2anb 497	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) → (𝐹 = 𝐺 ↔ (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥))))
5		fvex 6350	. . . 4 ⊢ (𝐹‘𝑥) ∈ V
6	5	rgenw 3050	. . 3 ⊢ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ V
7		mpteqb 6449	. . 3 ⊢ (∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ V → ((𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥)) ↔ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = (𝐺‘𝑥)))
8	6, 7	ax-mp 5	. 2 ⊢ ((𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥)) ↔ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = (𝐺‘𝑥))
9	4, 8	syl6bb 276	1 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) → (𝐹 = 𝐺 ↔ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = (𝐺‘𝑥)))

Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 383   = wceq 1620   ∈ wcel 2127  ∀wral 3038  Vcvv 3328   ↦ cmpt 4869   Fn wfn 6032  ‘cfv 6037

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1859  ax-4 1874  ax-5 1976  ax-6 2042  ax-7 2078  ax-8 2129  ax-9 2136  ax-10 2156  ax-11 2171  ax-12 2184  ax-13 2379  ax-ext 2728  ax-sep 4921  ax-nul 4929  ax-pow 4980  ax-pr 5043

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1623  df-ex 1842  df-nf 1847  df-sb 2035  df-eu 2599  df-mo 2600  df-clab 2735  df-cleq 2741  df-clel 2744  df-nfc 2879  df-ral 3043  df-rex 3044  df-rab 3047  df-v 3330  df-sbc 3565  df-csb 3663  df-dif 3706  df-un 3708  df-in 3710  df-ss 3717  df-nul 4047  df-if 4219  df-sn 4310  df-pr 4312  df-op 4316  df-uni 4577  df-br 4793  df-opab 4853  df-mpt 4870  df-id 5162  df-xp 5260  df-rel 5261  df-cnv 5262  df-co 5263  df-dm 5264  df-rn 5265  df-res 5266  df-ima 5267  df-iota 6000  df-fun 6039  df-fn 6040  df-fv 6045

This theorem is referenced by:  eqfnfv2  6463  eqfnfvd  6465  eqfnfv2f  6466  fvreseq0  6468  fnmptfvd  6471  fndmdifeq0  6474  fneqeql  6476  fnnfpeq0  6596  fconst2g  6620  cocan1  6697  cocan2  6698  weniso  6755  fnsuppres  7479  tfr3  7652  ixpfi2  8417  fipreima  8425  fseqenlem1  9008  fpwwe2lem8  9622  ofsubeq0  11180  ser0f  13019  hashgval2  13330  hashf1lem1  13402  prodf1f  14794  efcvgfsum  14986  prmreclem2  15794  1arithlem4  15803  1arith  15804  isgrpinv  17644  dprdf11  18593  psrbagconf1o  19547  islindf4  20350  pthaus  21614  xkohaus  21629  cnmpt11  21639  cnmpt21  21647  prdsxmetlem  22345  rrxmet  23362  rolle  23923  tdeglem4  23990  resinf1o  24452  dchrelbas2  25132  dchreq  25153  eqeefv  25953  axlowdimlem14  26005  nmlno0lem  27928  phoeqi  27993  occllem  28442  dfiop2  28892  hoeq  28899  ho01i  28967  hoeq1  28969  kbpj  29095  nmlnop0iALT  29134  lnopco0i  29143  nlelchi  29200  rnbra  29246  kbass5  29259  hmopidmchi  29290  hmopidmpji  29291  pjssdif2i  29313  pjinvari  29330  bnj1542  31205  bnj580  31261  subfacp1lem3  31442  subfacp1lem5  31444  mrsubff1  31689  msubff1  31731  faclimlem1  31907  fprb  31947  rdgprc  31976  broucube  33725  cocanfo  33794  eqfnun  33798  sdclem2  33820  rrnmet  33910  rrnequiv  33916  ltrnid  35893  ltrneq2  35906  tendoeq1  36523  pw2f1ocnv  38075  caofcan  38993  addrcom  39150  fsneq  39866  dvnprodlem1  40633