MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  eqfnfv Structured version   Visualization version   GIF version

Theorem eqfnfv 6874
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
StepHypRef Expression
1 dffn5 6793 . . 3 (𝐹 Fn 𝐴𝐹 = (𝑥𝐴 ↦ (𝐹𝑥)))
2 dffn5 6793 . . 3 (𝐺 Fn 𝐴𝐺 = (𝑥𝐴 ↦ (𝐺𝑥)))
3 eqeq12 2756 . . 3 ((𝐹 = (𝑥𝐴 ↦ (𝐹𝑥)) ∧ 𝐺 = (𝑥𝐴 ↦ (𝐺𝑥))) → (𝐹 = 𝐺 ↔ (𝑥𝐴 ↦ (𝐹𝑥)) = (𝑥𝐴 ↦ (𝐺𝑥))))
41, 2, 3syl2anb 601 . 2 ((𝐹 Fn 𝐴𝐺 Fn 𝐴) → (𝐹 = 𝐺 ↔ (𝑥𝐴 ↦ (𝐹𝑥)) = (𝑥𝐴 ↦ (𝐺𝑥))))
5 fvex 6752 . . . 4 (𝐹𝑥) ∈ V
65rgenw 3076 . . 3 𝑥𝐴 (𝐹𝑥) ∈ V
7 mpteqb 6859 . . 3 (∀𝑥𝐴 (𝐹𝑥) ∈ V → ((𝑥𝐴 ↦ (𝐹𝑥)) = (𝑥𝐴 ↦ (𝐺𝑥)) ↔ ∀𝑥𝐴 (𝐹𝑥) = (𝐺𝑥)))
86, 7ax-mp 5 . 2 ((𝑥𝐴 ↦ (𝐹𝑥)) = (𝑥𝐴 ↦ (𝐺𝑥)) ↔ ∀𝑥𝐴 (𝐹𝑥) = (𝐺𝑥))
94, 8bitrdi 290 1 ((𝐹 Fn 𝐴𝐺 Fn 𝐴) → (𝐹 = 𝐺 ↔ ∀𝑥𝐴 (𝐹𝑥) = (𝐺𝑥)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399   = wceq 1543  wcel 2112  wral 3064  Vcvv 3423  cmpt 5152   Fn wfn 6396  cfv 6401
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2160  ax-12 2177  ax-ext 2710  ax-sep 5209  ax-nul 5216  ax-pr 5339
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2073  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2818  df-nfc 2889  df-ne 2944  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3425  df-sbc 3712  df-csb 3829  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4255  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-opab 5133  df-mpt 5153  df-id 5472  df-xp 5575  df-rel 5576  df-cnv 5577  df-co 5578  df-dm 5579  df-rn 5580  df-res 5581  df-ima 5582  df-iota 6359  df-fun 6403  df-fn 6404  df-fv 6409
This theorem is referenced by:  eqfnfv2  6875  eqfnfvd  6877  eqfnfv2f  6878  fvreseq0  6880  fnmptfvd  6883  fndmdifeq0  6886  fneqeql  6888  fnnfpeq0  7015  fprb  7031  fconst2g  7040  cocan1  7123  cocan2  7124  weniso  7185  fsplitfpar  7909  fnsuppres  7957  tfr3  8159  ixpfi2  9004  fipreima  9012  updjud  9580  fseqenlem1  9668  fpwwe2lem7  10281  ofsubeq0  11857  ser0f  13661  hashgval2  13978  hashf1lem1  14053  hashf1lem1OLD  14054  prodf1f  15489  efcvgfsum  15680  prmreclem2  16503  1arithlem4  16512  1arith  16513  smndex1n0mnd  18372  isgrpinv  18453  dprdf11  19443  frlmplusgvalb  20764  frlmvscavalb  20765  islindf4  20833  psrbagconf1o  20927  psrbagconf1oOLD  20928  pthaus  22567  xkohaus  22582  cnmpt11  22592  cnmpt21  22600  prdsxmetlem  23298  rrxmet  24337  rolle  24919  tdeglem4  24989  tdeglem4OLD  24990  resinf1o  25457  dchrelbas2  26150  dchreq  26171  eqeefv  27026  axlowdimlem14  27078  elntg2  27108  nmlno0lem  28906  phoeqi  28970  occllem  29416  dfiop2  29866  hoeq  29873  ho01i  29941  hoeq1  29943  kbpj  30069  nmlnop0iALT  30108  lnopco0i  30117  nlelchi  30174  rnbra  30220  kbass5  30233  hmopidmchi  30264  hmopidmpji  30265  pjssdif2i  30287  pjinvari  30304  bnj1542  32581  bnj580  32637  subfacp1lem3  32888  subfacp1lem5  32890  mrsubff1  33220  msubff1  33262  faclimlem1  33459  rdgprc  33520  broucube  35585  cocanfo  35650  eqfnun  35654  sdclem2  35674  rrnmet  35761  rrnequiv  35767  ltrnid  37923  ltrneq2  37936  tendoeq1  38552  sticksstones1  39866  pw2f1ocnv  40610  caofcan  41662  addrcom  41814  fsneq  42467  dvnprodlem1  43208  cfsetsnfsetf1  44271  cfsetsnfsetfo  44272  rrx2pnecoorneor  45780  rrx2linest  45807
  Copyright terms: Public domain W3C validator