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

Theorem eqfnfv 5583
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 5529 . . 3  |-  ( F  Fn  A  <->  F  =  ( x  e.  A  |->  ( F `  x
) ) )
2 dffn5 5529 . . 3  |-  ( G  Fn  A  <->  G  =  ( x  e.  A  |->  ( G `  x
) ) )
3 eqeq12 2296 . . 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 467 . 2  |-  ( ( F  Fn  A  /\  G  Fn  A )  ->  ( F  =  G  <-> 
( x  e.  A  |->  ( F `  x
) )  =  ( x  e.  A  |->  ( G `  x ) ) ) )
5 fvex 5499 . . . 4  |-  ( F `
 x )  e. 
_V
65rgenw 2611 . . 3  |-  A. x  e.  A  ( F `  x )  e.  _V
7 mpteqb 5575 . . 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 10 . 2  |-  ( ( x  e.  A  |->  ( F `  x ) )  =  ( x  e.  A  |->  ( G `
 x ) )  <->  A. x  e.  A  ( F `  x )  =  ( G `  x ) )
94, 8syl6bb 254 1  |-  ( ( F  Fn  A  /\  G  Fn  A )  ->  ( F  =  G  <->  A. x  e.  A  ( F `  x )  =  ( G `  x ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 6    <-> wb 178    /\ wa 360    = wceq 1624    e. wcel 1685   A.wral 2544   _Vcvv 2789    e. cmpt 4078    Fn wfn 5216   ` cfv 5221
This theorem is referenced by:  eqfnfv2  5584  eqfnfvd  5586  eqfnfv2f  5587  fvreseq  5589  fndmdifeq0  5592  fneqeql  5594  fconst2g  5689  fnsuppres  5693  cocan1  5762  cocan2  5763  weniso  5813  tfr3  6410  ixpfi2  7149  fipreima  7156  fseqenlem1  7646  fpwwe2lem8  8254  ofsubeq0  9738  ser0f  11093  hashgval2  11354  hashf1lem1  11387  efcvgfsum  12361  prmreclem2  12958  1arithlem4  12967  1arith  12968  isgrpinv  14526  dprdf11  15252  psrbagconf1o  16114  pthaus  17326  xkohaus  17341  cnmpt11  17351  cnmpt21  17359  prdsxmetlem  17926  rolle  19331  tdeglem4  19440  resinf1o  19892  dchrelbas2  20470  dchreq  20491  nmlno0lem  21363  phoeqi  21428  occllem  21874  dfiop2  22325  hoeq  22332  ho01i  22400  hoeq1  22402  kbpj  22528  nmlnop0iALT  22567  lnopco0i  22576  nlelchi  22633  rnbra  22679  kbass5  22692  hmopidmchi  22723  hmopidmpji  22724  pjssdif2i  22746  pjinvari  22763  subfacp1lem3  23117  subfacp1lem5  23119  fprb  23530  rdgprc  23552  eqeefv  23938  axlowdimlem14  23990  surjsec2  24519  repfuntw  24559  cocanfo  25773  eqfnun  25786  sdclem2  25851  rrnmet  25952  rrnequiv  25958  fnnfpeq0  26157  pw2f1ocnv  26529  islindf4  26707  caofcan  26939  addrcom  27079  bnj1542  28156  bnj580  28212  ltrnid  29591  ltrneq2  29604  tendoeq1  30220
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1534  ax-5 1545  ax-17 1604  ax-9 1637  ax-8 1645  ax-13 1687  ax-14 1689  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1867  ax-ext 2265  ax-sep 4142  ax-nul 4150  ax-pr 4213  ax-un 4511
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3an 938  df-tru 1312  df-ex 1530  df-nf 1533  df-sb 1632  df-eu 2148  df-mo 2149  df-clab 2271  df-cleq 2277  df-clel 2280  df-nfc 2409  df-ne 2449  df-ral 2549  df-rex 2550  df-rab 2553  df-v 2791  df-sbc 2993  df-csb 3083  df-dif 3156  df-un 3158  df-in 3160  df-ss 3167  df-nul 3457  df-if 3567  df-sn 3647  df-pr 3648  df-op 3650  df-uni 3829  df-br 4025  df-opab 4079  df-mpt 4080  df-id 4308  df-xp 4694  df-rel 4695  df-cnv 4696  df-co 4697  df-dm 4698  df-rn 4699  df-res 4700  df-ima 4701  df-fun 5223  df-fn 5224  df-fv 5229
  Copyright terms: Public domain W3C validator