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

Theorem eqfnfv 5989
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  |-  ( ( F  Fn  A  /\  G  Fn  A )  ->  ( F  =  G  <->  A. x  e.  A  ( F `  x )  =  ( G `  x ) ) )
Distinct variable groups:    x, A    x, F    x, G

Proof of Theorem eqfnfv
StepHypRef Expression
1 dffn5 5924 . . 3  |-  ( F  Fn  A  <->  F  =  ( x  e.  A  |->  ( F `  x
) ) )
2 dffn5 5924 . . 3  |-  ( G  Fn  A  <->  G  =  ( x  e.  A  |->  ( G `  x
) ) )
3 eqeq12 2442 . . 3  |-  ( ( F  =  ( x  e.  A  |->  ( F `
 x ) )  /\  G  =  ( x  e.  A  |->  ( G `  x ) ) )  ->  ( F  =  G  <->  ( x  e.  A  |->  ( F `
 x ) )  =  ( x  e.  A  |->  ( G `  x ) ) ) )
41, 2, 3syl2anb 482 . 2  |-  ( ( F  Fn  A  /\  G  Fn  A )  ->  ( F  =  G  <-> 
( x  e.  A  |->  ( F `  x
) )  =  ( x  e.  A  |->  ( G `  x ) ) ) )
5 fvex 5889 . . . 4  |-  ( F `
 x )  e. 
_V
65rgenw 2787 . . 3  |-  A. x  e.  A  ( F `  x )  e.  _V
7 mpteqb 5978 . . 3  |-  ( A. x  e.  A  ( F `  x )  e.  _V  ->  ( (
x  e.  A  |->  ( F `  x ) )  =  ( x  e.  A  |->  ( G `
 x ) )  <->  A. x  e.  A  ( F `  x )  =  ( G `  x ) ) )
86, 7ax-mp 5 . 2  |-  ( ( x  e.  A  |->  ( F `  x ) )  =  ( x  e.  A  |->  ( G `
 x ) )  <->  A. x  e.  A  ( F `  x )  =  ( G `  x ) )
94, 8syl6bb 265 1  |-  ( ( F  Fn  A  /\  G  Fn  A )  ->  ( F  =  G  <->  A. x  e.  A  ( F `  x )  =  ( G `  x ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 188    /\ wa 371    = wceq 1438    e. wcel 1869   A.wral 2776   _Vcvv 3082    |-> cmpt 4480    Fn wfn 5594   ` cfv 5599
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-5 1749  ax-6 1795  ax-7 1840  ax-8 1871  ax-9 1873  ax-10 1888  ax-11 1893  ax-12 1906  ax-13 2054  ax-ext 2401  ax-sep 4544  ax-nul 4553  ax-pow 4600  ax-pr 4658
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 985  df-tru 1441  df-ex 1661  df-nf 1665  df-sb 1788  df-eu 2270  df-mo 2271  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2573  df-ne 2621  df-ral 2781  df-rex 2782  df-rab 2785  df-v 3084  df-sbc 3301  df-csb 3397  df-dif 3440  df-un 3442  df-in 3444  df-ss 3451  df-nul 3763  df-if 3911  df-sn 3998  df-pr 4000  df-op 4004  df-uni 4218  df-br 4422  df-opab 4481  df-mpt 4482  df-id 4766  df-xp 4857  df-rel 4858  df-cnv 4859  df-co 4860  df-dm 4861  df-rn 4862  df-res 4863  df-ima 4864  df-iota 5563  df-fun 5601  df-fn 5602  df-fv 5607
This theorem is referenced by:  eqfnfv2  5990  eqfnfvd  5992  eqfnfv2f  5993  fvreseq0  5995  fnmptfvd  5998  fndmdifeq0  6001  fneqeql  6003  fnnfpeq0  6108  fconst2g  6132  cocan1  6202  cocan2  6203  weniso  6258  fnsuppres  6951  tfr3  7123  ixpfi2  7876  fipreima  7884  fseqenlem1  8457  fpwwe2lem8  9064  ofsubeq0  10608  ser0f  12267  hashgval2  12558  hashf1lem1  12617  prodf1f  13941  efcvgfsum  14133  prmreclem2  14854  1arithlem4  14863  1arith  14864  isgrpinv  16709  dprdf11  17649  psrbagconf1o  18591  islindf4  19388  pthaus  20645  xkohaus  20660  cnmpt11  20670  cnmpt21  20678  prdsxmetlem  21375  rrxmet  22354  rolle  22934  tdeglem4  23001  resinf1o  23477  dchrelbas2  24157  dchreq  24178  eqeefv  24925  axlowdimlem14  24977  nmlno0lem  26426  phoeqi  26491  occllem  26948  dfiop2  27398  hoeq  27405  ho01i  27473  hoeq1  27475  kbpj  27601  nmlnop0iALT  27640  lnopco0i  27649  nlelchi  27706  rnbra  27752  kbass5  27765  hmopidmchi  27796  hmopidmpji  27797  pjssdif2i  27819  pjinvari  27836  bnj1542  29670  bnj580  29726  subfacp1lem3  29907  subfacp1lem5  29909  mrsubff1  30154  msubff1  30196  faclimlem1  30380  fprb  30414  rdgprc  30442  broucube  31894  cocanfo  31964  eqfnun  31968  sdclem2  31991  rrnmet  32081  rrnequiv  32087  ltrnid  33625  ltrneq2  33638  tendoeq1  34256  pw2f1ocnv  35818  caofcan  36536  addrcom  36692  dvnprodlem1  37647
  Copyright terms: Public domain W3C validator