Theorem eqfnfv 6909

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 6828	. . 3 ⊢ (𝐹 Fn 𝐴 ↔ 𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)))
2		dffn5 6828	. . 3 ⊢ (𝐺 Fn 𝐴 ↔ 𝐺 = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥)))
3		eqeq12 2755	. . 3 ⊢ ((𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) ∧ 𝐺 = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥))) → (𝐹 = 𝐺 ↔ (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥))))
4	1, 2, 3	syl2anb 598	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) → (𝐹 = 𝐺 ↔ (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥))))
5		fvex 6787	. . . 4 ⊢ (𝐹‘𝑥) ∈ V
6	5	rgenw 3076	. . 3 ⊢ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ V
7		mpteqb 6894	. . 3 ⊢ (∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ V → ((𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥)) ↔ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = (𝐺‘𝑥)))
8	6, 7	ax-mp 5	. 2 ⊢ ((𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥)) ↔ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = (𝐺‘𝑥))
9	4, 8	bitrdi 287	1 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) → (𝐹 = 𝐺 ↔ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = (𝐺‘𝑥)))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   = wceq 1539   ∈ wcel 2106  ∀wral 3064  Vcvv 3432   ↦ cmpt 5157   Fn wfn 6428  ‘cfv 6433

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-sep 5223  ax-nul 5230  ax-pr 5352

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3434  df-sbc 3717  df-csb 3833  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-br 5075  df-opab 5137  df-mpt 5158  df-id 5489  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-rn 5600  df-res 5601  df-ima 5602  df-iota 6391  df-fun 6435  df-fn 6436  df-fv 6441

This theorem is referenced by:  eqfnfv2  6910  eqfnfvd  6912  eqfnfv2f  6913  fvreseq0  6915  fnmptfvd  6918  fndmdifeq0  6921  fneqeql  6923  fnnfpeq0  7050  fprb  7069  fconst2g  7078  cocan1  7163  cocan2  7164  weniso  7225  fsplitfpar  7959  fnsuppres  8007  tfr3  8230  ixpfi2  9117  fipreima  9125  updjud  9692  fseqenlem1  9780  fpwwe2lem7  10393  ofsubeq0  11970  ser0f  13776  hashgval2  14093  hashf1lem1  14168  hashf1lem1OLD  14169  prodf1f  15604  efcvgfsum  15795  prmreclem2  16618  1arithlem4  16627  1arith  16628  smndex1n0mnd  18551  isgrpinv  18632  dprdf11  19626  frlmplusgvalb  20976  frlmvscavalb  20977  islindf4  21045  psrbagconf1o  21139  psrbagconf1oOLD  21140  pthaus  22789  xkohaus  22804  cnmpt11  22814  cnmpt21  22822  prdsxmetlem  23521  rrxmet  24572  rolle  25154  tdeglem4  25224  tdeglem4OLD  25225  resinf1o  25692  dchrelbas2  26385  dchreq  26406  eqeefv  27271  axlowdimlem14  27323  elntg2  27353  nmlno0lem  29155  phoeqi  29219  occllem  29665  dfiop2  30115  hoeq  30122  ho01i  30190  hoeq1  30192  kbpj  30318  nmlnop0iALT  30357  lnopco0i  30366  nlelchi  30423  rnbra  30469  kbass5  30482  hmopidmchi  30513  hmopidmpji  30514  pjssdif2i  30536  pjinvari  30553  bnj1542  32837  bnj580  32893  subfacp1lem3  33144  subfacp1lem5  33146  mrsubff1  33476  msubff1  33518  faclimlem1  33709  rdgprc  33770  broucube  35811  cocanfo  35876  eqfnun  35880  sdclem2  35900  rrnmet  35987  rrnequiv  35993  ltrnid  38149  ltrneq2  38162  tendoeq1  38778  sticksstones1  40102  pw2f1ocnv  40859  caofcan  41941  addrcom  42093  fsneq  42746  dvnprodlem1  43487  cfsetsnfsetf1  44553  cfsetsnfsetfo  44554  rrx2pnecoorneor  46061  rrx2linest  46088