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

Theorem eqfnfv 5818
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 5758 . . 3  |-  ( F  Fn  A  <->  F  =  ( x  e.  A  |->  ( F `  x
) ) )
2 dffn5 5758 . . 3  |-  ( G  Fn  A  <->  G  =  ( x  e.  A  |->  ( G `  x
) ) )
3 eqeq12 2455 . . 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 479 . 2  |-  ( ( F  Fn  A  /\  G  Fn  A )  ->  ( F  =  G  <-> 
( x  e.  A  |->  ( F `  x
) )  =  ( x  e.  A  |->  ( G `  x ) ) ) )
5 fvex 5722 . . . 4  |-  ( F `
 x )  e. 
_V
65rgenw 2804 . . 3  |-  A. x  e.  A  ( F `  x )  e.  _V
7 mpteqb 5809 . . 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 1369    e. wcel 1756   A.wral 2736   _Vcvv 2993    e. cmpt 4371    Fn wfn 5434   ` cfv 5439
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4434  ax-nul 4442  ax-pow 4491  ax-pr 4552
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-ne 2622  df-ral 2741  df-rex 2742  df-rab 2745  df-v 2995  df-sbc 3208  df-csb 3310  df-dif 3352  df-un 3354  df-in 3356  df-ss 3363  df-nul 3659  df-if 3813  df-sn 3899  df-pr 3901  df-op 3905  df-uni 4113  df-br 4314  df-opab 4372  df-mpt 4373  df-id 4657  df-xp 4867  df-rel 4868  df-cnv 4869  df-co 4870  df-dm 4871  df-rn 4872  df-res 4873  df-ima 4874  df-iota 5402  df-fun 5441  df-fn 5442  df-fv 5447
This theorem is referenced by:  eqfnfv2  5819  eqfnfvd  5821  eqfnfv2f  5822  fvreseq0  5824  fnmptfvd  5827  fndmdifeq0  5830  fneqeql  5832  fnnfpeq0  5930  fconst2g  5953  fnsuppresOLD  5959  cocan1  6016  cocan2  6017  weniso  6066  fnsuppres  6737  tfr3  6879  ixpfi2  7630  fipreima  7638  fseqenlem1  8215  fpwwe2lem8  8825  ofsubeq0  10340  ser0f  11880  hashgval2  12162  hashf1lem1  12229  efcvgfsum  13392  prmreclem2  13999  1arithlem4  14008  1arith  14009  isgrpinv  15609  dprdf11  16535  dprdf11OLD  16542  psrbagconf1o  17466  islindf4  18289  pthaus  19233  xkohaus  19248  cnmpt11  19258  cnmpt21  19266  prdsxmetlem  19965  rrxmet  20929  rolle  21484  tdeglem4  21551  resinf1o  22014  dchrelbas2  22598  dchreq  22619  eqeefv  23171  axlowdimlem14  23223  nmlno0lem  24215  phoeqi  24280  occllem  24728  dfiop2  25179  hoeq  25186  ho01i  25254  hoeq1  25256  kbpj  25382  nmlnop0iALT  25421  lnopco0i  25430  nlelchi  25487  rnbra  25533  kbass5  25546  hmopidmchi  25577  hmopidmpji  25578  pjssdif2i  25600  pjinvari  25617  signstres  26998  subfacp1lem3  27092  subfacp1lem5  27094  prodf1f  27429  faclimlem1  27571  fprb  27606  rdgprc  27630  cocanfo  28637  eqfnun  28641  sdclem2  28664  rrnmet  28754  rrnequiv  28760  pw2f1ocnv  29412  caofcan  29623  addrcom  29757  bnj1542  31946  bnj580  32002  ltrnid  33875  ltrneq2  33888  tendoeq1  34504
  Copyright terms: Public domain W3C validator