Theorem eqfnfv 6985

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 6900	. . 3 ⊢ (𝐹 Fn 𝐴 ↔ 𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)))
2		dffn5 6900	. . 3 ⊢ (𝐺 Fn 𝐴 ↔ 𝐺 = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥)))
3		eqeq12 2754	. . 3 ⊢ ((𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) ∧ 𝐺 = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥))) → (𝐹 = 𝐺 ↔ (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥))))
4	1, 2, 3	syl2anb 599	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) → (𝐹 = 𝐺 ↔ (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥))))
5		fvex 6855	. . . 4 ⊢ (𝐹‘𝑥) ∈ V
6	5	rgenw 3056	. . 3 ⊢ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ V
7		mpteqb 6969	. . 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 1542   ∈ wcel 2114  ∀wral 3052  Vcvv 3442   ↦ cmpt 5181   Fn wfn 6495  ‘cfv 6500

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5243  ax-nul 5253  ax-pr 5379

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5527  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-iota 6456  df-fun 6502  df-fn 6503  df-fv 6508

This theorem is referenced by:  eqfnfv2  6986  eqfnfvd  6988  eqfnfv2f  6989  eqfnun  6991  fvreseq0  6992  fnmptfvd  6995  fndmdifeq0  6998  fneqeql  7000  fnnfpeq0  7134  fprb  7150  fconst2g  7159  cocan1  7247  cocan2  7248  weniso  7310  fsplitfpar  8070  fnsuppres  8143  tfr3  8340  ixpfi2  9262  fipreima  9270  updjud  9858  fseqenlem1  9946  fpwwe2lem7  10560  ofsubeq0  12154  ser0f  13990  hashgval2  14313  hashf1lem1  14390  prodf1f  15827  efcvgfsum  16021  prmreclem2  16857  1arithlem4  16866  1arith  16867  smndex1n0mnd  18849  isgrpinv  18935  dprdf11  19966  frlmplusgvalb  21736  frlmvscavalb  21737  islindf4  21805  psrbagconf1o  21897  pthaus  23594  xkohaus  23609  cnmpt11  23619  cnmpt21  23627  prdsxmetlem  24324  rrxmet  25376  rolle  25962  tdeglem4  26033  resinf1o  26513  dchrelbas2  27216  dchreq  27237  eqeefv  28988  axlowdimlem14  29040  elntg2  29070  nmlno0lem  30881  phoeqi  30945  occllem  31391  dfiop2  31841  hoeq  31848  ho01i  31916  hoeq1  31918  kbpj  32044  nmlnop0iALT  32083  lnopco0i  32092  nlelchi  32149  rnbra  32195  kbass5  32208  hmopidmchi  32239  hmopidmpji  32240  pjssdif2i  32262  pjinvari  32279  bnj1542  35033  bnj580  35089  subfacp1lem3  35398  subfacp1lem5  35400  mrsubff1  35730  msubff1  35772  faclimlem1  35959  rdgprc  36008  broucube  37905  cocanfo  37970  sdclem2  37993  rrnmet  38080  rrnequiv  38086  ltrnid  40511  ltrneq2  40524  tendoeq1  41140  sticksstones1  42516  pw2f1ocnv  43394  caofcan  44679  addrcom  44830  fsneq  45564  dvnprodlem1  46304  cfsetsnfsetf1  47419  cfsetsnfsetfo  47420  rrx2pnecoorneor  49075  rrx2linest  49102  dfinito4  49860