Theorem eqfnfv 7050

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 6966	. . 3 ⊢ (𝐹 Fn 𝐴 ↔ 𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)))
2		dffn5 6966	. . 3 ⊢ (𝐺 Fn 𝐴 ↔ 𝐺 = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥)))
3		eqeq12 2751	. . 3 ⊢ ((𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) ∧ 𝐺 = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥))) → (𝐹 = 𝐺 ↔ (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥))))
4	1, 2, 3	syl2anb 598	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) → (𝐹 = 𝐺 ↔ (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥))))
5		fvex 6919	. . . 4 ⊢ (𝐹‘𝑥) ∈ V
6	5	rgenw 3062	. . 3 ⊢ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ V
7		mpteqb 7034	. . 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 1536   ∈ wcel 2105  ∀wral 3058  Vcvv 3477   ↦ cmpt 5230   Fn wfn 6557  ‘cfv 6562

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pr 5437

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-ral 3059  df-rex 3068  df-rab 3433  df-v 3479  df-sbc 3791  df-csb 3908  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5582  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-iota 6515  df-fun 6564  df-fn 6565  df-fv 6570

This theorem is referenced by:  eqfnfv2  7051  eqfnfvd  7053  eqfnfv2f  7054  eqfnun  7056  fvreseq0  7057  fnmptfvd  7060  fndmdifeq0  7063  fneqeql  7065  fnnfpeq0  7197  fprb  7213  fconst2g  7222  cocan1  7310  cocan2  7311  weniso  7373  fsplitfpar  8141  fnsuppres  8214  tfr3  8437  ixpfi2  9387  fipreima  9395  updjud  9971  fseqenlem1  10061  fpwwe2lem7  10674  ofsubeq0  12260  ser0f  14092  hashgval2  14413  hashf1lem1  14490  prodf1f  15924  efcvgfsum  16118  prmreclem2  16950  1arithlem4  16959  1arith  16960  smndex1n0mnd  18937  isgrpinv  19023  dprdf11  20057  frlmplusgvalb  21806  frlmvscavalb  21807  islindf4  21875  psrbagconf1o  21966  pthaus  23661  xkohaus  23676  cnmpt11  23686  cnmpt21  23694  prdsxmetlem  24393  rrxmet  25455  rolle  26042  tdeglem4  26113  resinf1o  26592  dchrelbas2  27295  dchreq  27316  eqeefv  28932  axlowdimlem14  28984  elntg2  29014  nmlno0lem  30821  phoeqi  30885  occllem  31331  dfiop2  31781  hoeq  31788  ho01i  31856  hoeq1  31858  kbpj  31984  nmlnop0iALT  32023  lnopco0i  32032  nlelchi  32089  rnbra  32135  kbass5  32148  hmopidmchi  32179  hmopidmpji  32180  pjssdif2i  32202  pjinvari  32219  bnj1542  34849  bnj580  34905  subfacp1lem3  35166  subfacp1lem5  35168  mrsubff1  35498  msubff1  35540  faclimlem1  35722  rdgprc  35775  broucube  37640  cocanfo  37705  sdclem2  37728  rrnmet  37815  rrnequiv  37821  ltrnid  40117  ltrneq2  40130  tendoeq1  40746  sticksstones1  42127  pw2f1ocnv  43025  caofcan  44318  addrcom  44470  fsneq  45148  dvnprodlem1  45901  cfsetsnfsetf1  47008  cfsetsnfsetfo  47009  rrx2pnecoorneor  48564  rrx2linest  48591