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

Theorem eqfnfv 6277
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 6208 . . 3 (𝐹 Fn 𝐴𝐹 = (𝑥𝐴 ↦ (𝐹𝑥)))
2 dffn5 6208 . . 3 (𝐺 Fn 𝐴𝐺 = (𝑥𝐴 ↦ (𝐺𝑥)))
3 eqeq12 2634 . . 3 ((𝐹 = (𝑥𝐴 ↦ (𝐹𝑥)) ∧ 𝐺 = (𝑥𝐴 ↦ (𝐺𝑥))) → (𝐹 = 𝐺 ↔ (𝑥𝐴 ↦ (𝐹𝑥)) = (𝑥𝐴 ↦ (𝐺𝑥))))
41, 2, 3syl2anb 496 . 2 ((𝐹 Fn 𝐴𝐺 Fn 𝐴) → (𝐹 = 𝐺 ↔ (𝑥𝐴 ↦ (𝐹𝑥)) = (𝑥𝐴 ↦ (𝐺𝑥))))
5 fvex 6168 . . . 4 (𝐹𝑥) ∈ V
65rgenw 2920 . . 3 𝑥𝐴 (𝐹𝑥) ∈ V
7 mpteqb 6265 . . 3 (∀𝑥𝐴 (𝐹𝑥) ∈ V → ((𝑥𝐴 ↦ (𝐹𝑥)) = (𝑥𝐴 ↦ (𝐺𝑥)) ↔ ∀𝑥𝐴 (𝐹𝑥) = (𝐺𝑥)))
86, 7ax-mp 5 . 2 ((𝑥𝐴 ↦ (𝐹𝑥)) = (𝑥𝐴 ↦ (𝐺𝑥)) ↔ ∀𝑥𝐴 (𝐹𝑥) = (𝐺𝑥))
94, 8syl6bb 276 1 ((𝐹 Fn 𝐴𝐺 Fn 𝐴) → (𝐹 = 𝐺 ↔ ∀𝑥𝐴 (𝐹𝑥) = (𝐺𝑥)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384   = wceq 1480  wcel 1987  wral 2908  Vcvv 3190  cmpt 4683   Fn wfn 5852  cfv 5857
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-sep 4751  ax-nul 4759  ax-pow 4813  ax-pr 4877
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ral 2913  df-rex 2914  df-rab 2917  df-v 3192  df-sbc 3423  df-csb 3520  df-dif 3563  df-un 3565  df-in 3567  df-ss 3574  df-nul 3898  df-if 4065  df-sn 4156  df-pr 4158  df-op 4162  df-uni 4410  df-br 4624  df-opab 4684  df-mpt 4685  df-id 4999  df-xp 5090  df-rel 5091  df-cnv 5092  df-co 5093  df-dm 5094  df-rn 5095  df-res 5096  df-ima 5097  df-iota 5820  df-fun 5859  df-fn 5860  df-fv 5865
This theorem is referenced by:  eqfnfv2  6278  eqfnfvd  6280  eqfnfv2f  6281  fvreseq0  6283  fnmptfvd  6286  fndmdifeq0  6289  fneqeql  6291  fnnfpeq0  6409  fconst2g  6433  cocan1  6511  cocan2  6512  weniso  6569  fnsuppres  7282  tfr3  7455  ixpfi2  8224  fipreima  8232  fseqenlem1  8807  fpwwe2lem8  9419  ofsubeq0  10977  ser0f  12810  hashgval2  13123  hashf1lem1  13193  prodf1f  14568  efcvgfsum  14760  prmreclem2  15564  1arithlem4  15573  1arith  15574  isgrpinv  17412  dprdf11  18362  psrbagconf1o  19314  islindf4  20117  pthaus  21381  xkohaus  21396  cnmpt11  21406  cnmpt21  21414  prdsxmetlem  22113  rrxmet  23131  rolle  23691  tdeglem4  23758  resinf1o  24220  dchrelbas2  24896  dchreq  24917  eqeefv  25717  axlowdimlem14  25769  nmlno0lem  27536  phoeqi  27601  occllem  28050  dfiop2  28500  hoeq  28507  ho01i  28575  hoeq1  28577  kbpj  28703  nmlnop0iALT  28742  lnopco0i  28751  nlelchi  28808  rnbra  28854  kbass5  28867  hmopidmchi  28898  hmopidmpji  28899  pjssdif2i  28921  pjinvari  28938  bnj1542  30688  bnj580  30744  subfacp1lem3  30925  subfacp1lem5  30927  mrsubff1  31172  msubff1  31214  faclimlem1  31390  fprb  31426  rdgprc  31454  broucube  33114  cocanfo  33183  eqfnun  33187  sdclem2  33209  rrnmet  33299  rrnequiv  33305  ltrnid  34940  ltrneq2  34953  tendoeq1  35571  pw2f1ocnv  37123  caofcan  38043  addrcom  38200  fsneq  38907  dvnprodlem1  39498
  Copyright terms: Public domain W3C validator