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

Theorem eqfnfv 5785
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 5725 . . 3  |-  ( F  Fn  A  <->  F  =  ( x  e.  A  |->  ( F `  x
) ) )
2 dffn5 5725 . . 3  |-  ( G  Fn  A  <->  G  =  ( x  e.  A  |->  ( G `  x
) ) )
3 eqeq12 2445 . . 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 476 . 2  |-  ( ( F  Fn  A  /\  G  Fn  A )  ->  ( F  =  G  <-> 
( x  e.  A  |->  ( F `  x
) )  =  ( x  e.  A  |->  ( G `  x ) ) ) )
5 fvex 5689 . . . 4  |-  ( F `
 x )  e. 
_V
65rgenw 2773 . . 3  |-  A. x  e.  A  ( F `  x )  e.  _V
7 mpteqb 5776 . . 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 261 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 184    /\ wa 369    = wceq 1362    e. wcel 1755   A.wral 2705   _Vcvv 2962    e. cmpt 4338    Fn wfn 5401   ` cfv 5406
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-8 1757  ax-9 1759  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414  ax-sep 4401  ax-nul 4409  ax-pow 4458  ax-pr 4519
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 960  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-eu 2258  df-mo 2259  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-ne 2598  df-ral 2710  df-rex 2711  df-rab 2714  df-v 2964  df-sbc 3176  df-csb 3277  df-dif 3319  df-un 3321  df-in 3323  df-ss 3330  df-nul 3626  df-if 3780  df-sn 3866  df-pr 3868  df-op 3872  df-uni 4080  df-br 4281  df-opab 4339  df-mpt 4340  df-id 4623  df-xp 4833  df-rel 4834  df-cnv 4835  df-co 4836  df-dm 4837  df-rn 4838  df-res 4839  df-ima 4840  df-iota 5369  df-fun 5408  df-fn 5409  df-fv 5414
This theorem is referenced by:  eqfnfv2  5786  eqfnfvd  5788  eqfnfv2f  5789  fvreseq0  5791  fnmptfvd  5794  fndmdifeq0  5797  fneqeql  5799  fnnfpeq0  5896  fconst2g  5919  fnsuppresOLD  5925  cocan1  5982  cocan2  5983  weniso  6032  fnsuppres  6705  tfr3  6844  ixpfi2  7597  fipreima  7605  fseqenlem1  8182  fpwwe2lem8  8791  ofsubeq0  10306  ser0f  11842  hashgval2  12124  hashf1lem1  12191  efcvgfsum  13353  prmreclem2  13960  1arithlem4  13969  1arith  13970  isgrpinv  15567  dprdf11  16486  dprdf11OLD  16493  psrbagconf1o  17377  islindf4  18108  pthaus  19052  xkohaus  19067  cnmpt11  19077  cnmpt21  19085  prdsxmetlem  19784  rrxmet  20748  rolle  21303  tdeglem4  21413  resinf1o  21876  dchrelbas2  22460  dchreq  22481  eqeefv  22971  axlowdimlem14  23023  nmlno0lem  24015  phoeqi  24080  occllem  24528  dfiop2  24979  hoeq  24986  ho01i  25054  hoeq1  25056  kbpj  25182  nmlnop0iALT  25221  lnopco0i  25230  nlelchi  25287  rnbra  25333  kbass5  25346  hmopidmchi  25377  hmopidmpji  25378  pjssdif2i  25400  pjinvari  25417  signstres  26823  subfacp1lem3  26917  subfacp1lem5  26919  prodf1f  27253  faclimlem1  27395  fprb  27430  rdgprc  27454  cocanfo  28452  eqfnun  28456  sdclem2  28479  rrnmet  28569  rrnequiv  28575  pw2f1ocnv  29228  caofcan  29439  addrcom  29573  bnj1542  31549  bnj580  31605  ltrnid  33349  ltrneq2  33362  tendoeq1  33978
  Copyright terms: Public domain W3C validator