Theorem eqfnfv 7064

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 6980	. . 3 ⊢ (𝐹 Fn 𝐴 ↔ 𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)))
2		dffn5 6980	. . 3 ⊢ (𝐺 Fn 𝐴 ↔ 𝐺 = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥)))
3		eqeq12 2757	. . 3 ⊢ ((𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) ∧ 𝐺 = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥))) → (𝐹 = 𝐺 ↔ (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥))))
4	1, 2, 3	syl2anb 597	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) → (𝐹 = 𝐺 ↔ (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥))))
5		fvex 6933	. . . 4 ⊢ (𝐹‘𝑥) ∈ V
6	5	rgenw 3071	. . 3 ⊢ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ V
7		mpteqb 7048	. . 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 1537   ∈ wcel 2108  ∀wral 3067  Vcvv 3488   ↦ cmpt 5249   Fn wfn 6568  ‘cfv 6573

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711  ax-sep 5317  ax-nul 5324  ax-pr 5447

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2543  df-eu 2572  df-clab 2718  df-cleq 2732  df-clel 2819  df-nfc 2895  df-ne 2947  df-ral 3068  df-rex 3077  df-rab 3444  df-v 3490  df-sbc 3805  df-csb 3922  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-br 5167  df-opab 5229  df-mpt 5250  df-id 5593  df-xp 5706  df-rel 5707  df-cnv 5708  df-co 5709  df-dm 5710  df-rn 5711  df-res 5712  df-ima 5713  df-iota 6525  df-fun 6575  df-fn 6576  df-fv 6581

This theorem is referenced by:  eqfnfv2  7065  eqfnfvd  7067  eqfnfv2f  7068  eqfnun  7070  fvreseq0  7071  fnmptfvd  7074  fndmdifeq0  7077  fneqeql  7079  fnnfpeq0  7212  fprb  7231  fconst2g  7240  cocan1  7327  cocan2  7328  weniso  7390  fsplitfpar  8159  fnsuppres  8232  tfr3  8455  ixpfi2  9420  fipreima  9428  updjud  10003  fseqenlem1  10093  fpwwe2lem7  10706  ofsubeq0  12290  ser0f  14106  hashgval2  14427  hashf1lem1  14504  prodf1f  15940  efcvgfsum  16134  prmreclem2  16964  1arithlem4  16973  1arith  16974  smndex1n0mnd  18947  isgrpinv  19033  dprdf11  20067  frlmplusgvalb  21812  frlmvscavalb  21813  islindf4  21881  psrbagconf1o  21972  pthaus  23667  xkohaus  23682  cnmpt11  23692  cnmpt21  23700  prdsxmetlem  24399  rrxmet  25461  rolle  26048  tdeglem4  26119  resinf1o  26596  dchrelbas2  27299  dchreq  27320  eqeefv  28936  axlowdimlem14  28988  elntg2  29018  nmlno0lem  30825  phoeqi  30889  occllem  31335  dfiop2  31785  hoeq  31792  ho01i  31860  hoeq1  31862  kbpj  31988  nmlnop0iALT  32027  lnopco0i  32036  nlelchi  32093  rnbra  32139  kbass5  32152  hmopidmchi  32183  hmopidmpji  32184  pjssdif2i  32206  pjinvari  32223  bnj1542  34833  bnj580  34889  subfacp1lem3  35150  subfacp1lem5  35152  mrsubff1  35482  msubff1  35524  faclimlem1  35705  rdgprc  35758  broucube  37614  cocanfo  37679  sdclem2  37702  rrnmet  37789  rrnequiv  37795  ltrnid  40092  ltrneq2  40105  tendoeq1  40721  sticksstones1  42103  pw2f1ocnv  42994  caofcan  44292  addrcom  44444  fsneq  45113  dvnprodlem1  45867  cfsetsnfsetf1  46974  cfsetsnfsetfo  46975  rrx2pnecoorneor  48449  rrx2linest  48476