Theorem eqfnfv 7029

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 6943	. . 3 ⊢ (𝐹 Fn 𝐴 ↔ 𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)))
2		dffn5 6943	. . 3 ⊢ (𝐺 Fn 𝐴 ↔ 𝐺 = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥)))
3		eqeq12 2782	. . 3 ⊢ ((𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) ∧ 𝐺 = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥))) → (𝐹 = 𝐺 ↔ (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥))))
4	1, 2, 3	syl2anb 610	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) → (𝐹 = 𝐺 ↔ (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥))))
5		fvex 6898	. . . 4 ⊢ (𝐹‘𝑥) ∈ V
6	5	rgenw 3085	. . 3 ⊢ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ V
7		mpteqb 7013	. . 3 ⊢ (∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ V → ((𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥)) ↔ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = (𝐺‘𝑥)))
8	6, 7	ax-mp 5	. 2 ⊢ ((𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥)) ↔ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = (𝐺‘𝑥))
9	4, 8	bitrdi 290	1 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) → (𝐹 = 𝐺 ↔ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = (𝐺‘𝑥)))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1570   ∈ wcel 2146  ∀wral 3081  Vcvv 3457   ↦ cmpt 5194   Fn wfn 6535  ‘cfv 6540

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2737  ax-sep 5259  ax-nul 5271  ax-pr 5406

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2569  df-eu 2599  df-clab 2744  df-cleq 2757  df-clel 2840  df-nfc 2914  df-ne 2961  df-ral 3082  df-rex 3092  df-rab 3419  df-v 3459  df-sbc 3747  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-opab 5176  df-mpt 5195  df-id 5558  df-xp 5669  df-rel 5670  df-cnv 5671  df-co 5672  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676  df-iota 6496  df-fun 6542  df-fn 6543  df-fv 6548

This theorem is used by:  eqfnfv2  7030  eqfnfvd  7032  eqfnfv2f  7033  fsneq  7034  eqfnun  7036  fvreseq0  7037  fnmptfvd  7040  fndmdifeq0  7043  fneqeql  7045  fnnfpeq0  7182  fprb  7198  fconst2g  7208  cocan1  7298  cocan2  7299  weniso  7363  fsplitfpar  8119  fnsuppres  8193  tfr3  8392  ixpfi2  9314  fipreima  9322  updjud  9936  fseqenlem1  10024  fpwwe2lem7  10639  ofsubeq0  12232  ser0f  14111  hashgval2  14434  hashf1lem1  14512  prodf1f  15971  efcvgfsum  16164  prmreclem2  17001  1arithlem4  17010  1arith  17011  smndex1n0mnd  19013  isgrpinv  19106  dprdf11  20141  frlmplusgvalb  21971  frlmvscavalb  21972  islindf4  22040  psrbagconf1o  22131  pthaus  23848  xkohaus  23863  cnmpt11  23873  cnmpt21  23881  prdsxmetlem  24578  rrxmet  25620  rolle  26202  tdeglem4  26270  resinf1o  26754  dchrelbas2  27454  dchreq  27475  eqeefv  29310  axlowdimlem14  29362  elntg2  29392  nmlno0lem  31218  phoeqi  31282  occllem  31728  dfiop2  32178  hoeq  32185  ho01i  32253  hoeq1  32255  kbpj  32381  nmlnop0iALT  32420  lnopco0i  32429  nlelchi  32486  rnbra  32532  kbass5  32545  hmopidmchi  32576  hmopidmpji  32577  pjssdif2i  32599  pjinvari  32616  bnj1542  35312  bnj580  35368  subfacp1lem3  35713  subfacp1lem5  35715  mrsubff1  36045  msubff1  36087  faclimlem1  36274  rdgprc  36323  broucube  38364  cocanfo  38430  sdclem2  38453  rrnmet  38540  rrnequiv  38546  ltrnid  40969  ltrneq2  40982  tendoeq1  41598  sticksstones1  42973  pw2f1ocnv  43824  caofcan  45093  addrcom  45243  dvnprodlem1  46720  cfsetsnfsetf1  47856  cfsetsnfsetfo  47857  rrx2pnecoorneor  49554  rrx2linest  49581  dfinito4  50338