Theorem eqfnfv 6974

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 6890	. . 3 ⊢ (𝐹 Fn 𝐴 ↔ 𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)))
2		dffn5 6890	. . 3 ⊢ (𝐺 Fn 𝐴 ↔ 𝐺 = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥)))
3		eqeq12 2751	. . 3 ⊢ ((𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) ∧ 𝐺 = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥))) → (𝐹 = 𝐺 ↔ (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥))))
4	1, 2, 3	syl2anb 598	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) → (𝐹 = 𝐺 ↔ (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥))))
5		fvex 6845	. . . 4 ⊢ (𝐹‘𝑥) ∈ V
6	5	rgenw 3053	. . 3 ⊢ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ V
7		mpteqb 6958	. . 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 1541   ∈ wcel 2113  ∀wral 3049  Vcvv 3438   ↦ cmpt 5177   Fn wfn 6485  ‘cfv 6490

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2706  ax-sep 5239  ax-nul 5249  ax-pr 5375

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2809  df-nfc 2883  df-ne 2931  df-ral 3050  df-rex 3059  df-rab 3398  df-v 3440  df-sbc 3739  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4284  df-if 4478  df-sn 4579  df-pr 4581  df-op 4585  df-uni 4862  df-br 5097  df-opab 5159  df-mpt 5178  df-id 5517  df-xp 5628  df-rel 5629  df-cnv 5630  df-co 5631  df-dm 5632  df-rn 5633  df-res 5634  df-ima 5635  df-iota 6446  df-fun 6492  df-fn 6493  df-fv 6498

This theorem is referenced by:  eqfnfv2  6975  eqfnfvd  6977  eqfnfv2f  6978  eqfnun  6980  fvreseq0  6981  fnmptfvd  6984  fndmdifeq0  6987  fneqeql  6989  fnnfpeq0  7122  fprb  7138  fconst2g  7147  cocan1  7235  cocan2  7236  weniso  7298  fsplitfpar  8058  fnsuppres  8131  tfr3  8328  ixpfi2  9248  fipreima  9256  updjud  9844  fseqenlem1  9932  fpwwe2lem7  10546  ofsubeq0  12140  ser0f  13976  hashgval2  14299  hashf1lem1  14376  prodf1f  15813  efcvgfsum  16007  prmreclem2  16843  1arithlem4  16852  1arith  16853  smndex1n0mnd  18835  isgrpinv  18921  dprdf11  19952  frlmplusgvalb  21722  frlmvscavalb  21723  islindf4  21791  psrbagconf1o  21883  pthaus  23580  xkohaus  23595  cnmpt11  23605  cnmpt21  23613  prdsxmetlem  24310  rrxmet  25362  rolle  25948  tdeglem4  26019  resinf1o  26499  dchrelbas2  27202  dchreq  27223  eqeefv  28925  axlowdimlem14  28977  elntg2  29007  nmlno0lem  30817  phoeqi  30881  occllem  31327  dfiop2  31777  hoeq  31784  ho01i  31852  hoeq1  31854  kbpj  31980  nmlnop0iALT  32019  lnopco0i  32028  nlelchi  32085  rnbra  32131  kbass5  32144  hmopidmchi  32175  hmopidmpji  32176  pjssdif2i  32198  pjinvari  32215  bnj1542  34962  bnj580  35018  subfacp1lem3  35325  subfacp1lem5  35327  mrsubff1  35657  msubff1  35699  faclimlem1  35886  rdgprc  35935  broucube  37794  cocanfo  37859  sdclem2  37882  rrnmet  37969  rrnequiv  37975  ltrnid  40334  ltrneq2  40347  tendoeq1  40963  sticksstones1  42339  pw2f1ocnv  43221  caofcan  44506  addrcom  44657  fsneq  45392  dvnprodlem1  46132  cfsetsnfsetf1  47247  cfsetsnfsetfo  47248  rrx2pnecoorneor  48903  rrx2linest  48930  dfinito4  49688