Theorem eqfnfv 6043

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 5975	. . 3 ⊢ (𝐹 Fn 𝐴 ↔ 𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)))
2		dffn5 5975	. . 3 ⊢ (𝐺 Fn 𝐴 ↔ 𝐺 = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥)))
3		eqeq12 2518	. . 3 ⊢ ((𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) ∧ 𝐺 = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥))) → (𝐹 = 𝐺 ↔ (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥))))
4	1, 2, 3	syl2anb 489	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) → (𝐹 = 𝐺 ↔ (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥))))
5		fvex 5937	. . . 4 ⊢ (𝐹‘𝑥) ∈ V
6	5	rgenw 2803	. . 3 ⊢ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ V
7		mpteqb 6031	. . 3 ⊢ (∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ V → ((𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥)) ↔ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = (𝐺‘𝑥)))
8	6, 7	ax-mp 5	. 2 ⊢ ((𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥)) ↔ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = (𝐺‘𝑥))
9	4, 8	syl6bb 271	1 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) → (𝐹 = 𝐺 ↔ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = (𝐺‘𝑥)))

Syntax hints:   → wi 4   ↔ wb 191   ∧ wa 378   = wceq 1468   ∈ wcel 1937  ∀wral 2791  Vcvv 3066   ↦ cmpt 4493   Fn wfn 5628  ‘cfv 5633

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1698  ax-4 1711  ax-5 1789  ax-6 1836  ax-7 1883  ax-8 1939  ax-9 1946  ax-10 1965  ax-11 1970  ax-12 1983  ax-13 2137  ax-ext 2485  ax-sep 4558  ax-nul 4567  ax-pow 4619  ax-pr 4680

This theorem depends on definitions:  df-bi 192  df-or 379  df-an 380  df-3an 1023  df-tru 1471  df-ex 1693  df-nf 1697  df-sb 1829  df-eu 2357  df-mo 2358  df-clab 2492  df-cleq 2498  df-clel 2501  df-nfc 2635  df-ne 2677  df-ral 2796  df-rex 2797  df-rab 2800  df-v 3068  df-sbc 3292  df-csb 3386  df-dif 3429  df-un 3431  df-in 3433  df-ss 3440  df-nul 3758  df-if 3909  df-sn 3996  df-pr 3998  df-op 4002  df-uni 4229  df-br 4435  df-opab 4494  df-mpt 4495  df-id 4795  df-xp 4886  df-rel 4887  df-cnv 4888  df-co 4889  df-dm 4890  df-rn 4891  df-res 4892  df-ima 4893  df-iota 5597  df-fun 5635  df-fn 5636  df-fv 5641

This theorem is referenced by:  eqfnfv2  6044  eqfnfvd  6046  eqfnfv2f  6047  fvreseq0  6049  fnmptfvd  6052  fndmdifeq0  6055  fneqeql  6057  fnnfpeq0  6163  fconst2g  6187  cocan1  6260  cocan2  6261  weniso  6318  fnsuppres  7020  tfr3  7194  ixpfi2  7957  fipreima  7965  fseqenlem1  8540  fpwwe2lem8  9147  ofsubeq0  10695  ser0f  12380  hashgval2  12675  hashf1lem1  12741  prodf1f  14108  efcvgfsum  14300  prmreclem2  15023  1arithlem4  15032  1arith  15033  isgrpinv  16876  dprdf11  17816  psrbagconf1o  18757  islindf4  19554  pthaus  20810  xkohaus  20825  cnmpt11  20835  cnmpt21  20843  prdsxmetlem  21541  rrxmet  22521  rolle  23103  tdeglem4  23170  resinf1o  23646  dchrelbas2  24326  dchreq  24347  eqeefv  25094  axlowdimlem14  25146  nmlno0lem  26597  phoeqi  26662  occllem  27119  dfiop2  27569  hoeq  27576  ho01i  27644  hoeq1  27646  kbpj  27772  nmlnop0iALT  27811  lnopco0i  27820  nlelchi  27877  rnbra  27923  kbass5  27936  hmopidmchi  27967  hmopidmpji  27968  pjssdif2i  27990  pjinvari  28007  bnj1542  29820  bnj580  29876  subfacp1lem3  30057  subfacp1lem5  30059  mrsubff1  30304  msubff1  30346  faclimlem1  30530  fprb  30564  rdgprc  30592  broucube  32212  cocanfo  32282  eqfnun  32286  sdclem2  32308  rrnmet  32398  rrnequiv  32404  ltrnid  33940  ltrneq2  33953  tendoeq1  34571  pw2f1ocnv  36132  caofcan  37029  addrcom  37185  fsneq  37846  dvnprodlem1  38240