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

Theorem eqfnfv 6797
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 6719 . . 3 (𝐹 Fn 𝐴𝐹 = (𝑥𝐴 ↦ (𝐹𝑥)))
2 dffn5 6719 . . 3 (𝐺 Fn 𝐴𝐺 = (𝑥𝐴 ↦ (𝐺𝑥)))
3 eqeq12 2835 . . 3 ((𝐹 = (𝑥𝐴 ↦ (𝐹𝑥)) ∧ 𝐺 = (𝑥𝐴 ↦ (𝐺𝑥))) → (𝐹 = 𝐺 ↔ (𝑥𝐴 ↦ (𝐹𝑥)) = (𝑥𝐴 ↦ (𝐺𝑥))))
41, 2, 3syl2anb 599 . 2 ((𝐹 Fn 𝐴𝐺 Fn 𝐴) → (𝐹 = 𝐺 ↔ (𝑥𝐴 ↦ (𝐹𝑥)) = (𝑥𝐴 ↦ (𝐺𝑥))))
5 fvex 6678 . . . 4 (𝐹𝑥) ∈ V
65rgenw 3150 . . 3 𝑥𝐴 (𝐹𝑥) ∈ V
7 mpteqb 6782 . . 3 (∀𝑥𝐴 (𝐹𝑥) ∈ V → ((𝑥𝐴 ↦ (𝐹𝑥)) = (𝑥𝐴 ↦ (𝐺𝑥)) ↔ ∀𝑥𝐴 (𝐹𝑥) = (𝐺𝑥)))
86, 7ax-mp 5 . 2 ((𝑥𝐴 ↦ (𝐹𝑥)) = (𝑥𝐴 ↦ (𝐺𝑥)) ↔ ∀𝑥𝐴 (𝐹𝑥) = (𝐺𝑥))
94, 8syl6bb 289 1 ((𝐹 Fn 𝐴𝐺 Fn 𝐴) → (𝐹 = 𝐺 ↔ ∀𝑥𝐴 (𝐹𝑥) = (𝐺𝑥)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 208  wa 398   = wceq 1533  wcel 2110  wral 3138  Vcvv 3495  cmpt 5139   Fn wfn 6345  cfv 6350
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2156  ax-12 2172  ax-ext 2793  ax-sep 5196  ax-nul 5203  ax-pow 5259  ax-pr 5322
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3497  df-sbc 3773  df-csb 3884  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4833  df-br 5060  df-opab 5122  df-mpt 5140  df-id 5455  df-xp 5556  df-rel 5557  df-cnv 5558  df-co 5559  df-dm 5560  df-rn 5561  df-res 5562  df-ima 5563  df-iota 6309  df-fun 6352  df-fn 6353  df-fv 6358
This theorem is referenced by:  eqfnfv2  6798  eqfnfvd  6800  eqfnfv2f  6801  fvreseq0  6803  fnmptfvd  6806  fndmdifeq0  6809  fneqeql  6811  fnnfpeq0  6935  fprb  6951  fconst2g  6960  cocan1  7041  cocan2  7042  weniso  7101  fsplitfpar  7808  fnsuppres  7851  tfr3  8029  ixpfi2  8816  fipreima  8824  updjud  9357  fseqenlem1  9444  fpwwe2lem8  10053  ofsubeq0  11629  ser0f  13417  hashgval2  13733  hashf1lem1  13807  prodf1f  15242  efcvgfsum  15433  prmreclem2  16247  1arithlem4  16256  1arith  16257  smndex1n0mnd  18071  isgrpinv  18150  dprdf11  19139  psrbagconf1o  20148  frlmplusgvalb  20907  frlmvscavalb  20908  islindf4  20976  pthaus  22240  xkohaus  22255  cnmpt11  22265  cnmpt21  22273  prdsxmetlem  22972  rrxmet  24005  rolle  24581  tdeglem4  24648  resinf1o  25114  dchrelbas2  25807  dchreq  25828  eqeefv  26683  axlowdimlem14  26735  elntg2  26765  nmlno0lem  28564  phoeqi  28628  occllem  29074  dfiop2  29524  hoeq  29531  ho01i  29599  hoeq1  29601  kbpj  29727  nmlnop0iALT  29766  lnopco0i  29775  nlelchi  29832  rnbra  29878  kbass5  29891  hmopidmchi  29922  hmopidmpji  29923  pjssdif2i  29945  pjinvari  29962  bnj1542  32124  bnj580  32180  subfacp1lem3  32424  subfacp1lem5  32426  mrsubff1  32756  msubff1  32798  faclimlem1  32970  rdgprc  33034  broucube  34920  cocanfo  34987  eqfnun  34991  sdclem2  35011  rrnmet  35101  rrnequiv  35107  ltrnid  37265  ltrneq2  37278  tendoeq1  37894  pw2f1ocnv  39627  caofcan  40648  addrcom  40800  fsneq  41461  dvnprodlem1  42223  rrx2pnecoorneor  44695  rrx2linest  44722
  Copyright terms: Public domain W3C validator