Theorem eqfnfv 6311

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

Step	Hyp	Ref	Expression
1		dffn5 6241	. . 3 |- ( F Fn A <-> F = ( x e. A |-> ( F ` x ) ) )
2		dffn5 6241	. . 3 |- ( G Fn A <-> G = ( x e. A |-> ( G ` x ) ) )
3		eqeq12 2635	. . 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 ) ) ) )
4	1, 2, 3	syl2anb 496	. 2 |- ( ( F Fn A /\ G Fn A ) -> ( F = G <-> ( x e. A |-> ( F ` x ) ) = ( x e. A |-> ( G ` x ) ) ) )
5		fvex 6201	. . . 4 |- ( F ` x ) e. _V
6	5	rgenw 2924	. . 3 |- A. x e. A ( F ` x ) e. _V
7		mpteqb 6299	. . 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 ) ) )
8	6, 7	ax-mp 5	. 2 |- ( ( x e. A |-> ( F ` x ) ) = ( x e. A |-> ( G ` x ) ) <-> A. x e. A ( F ` x ) = ( G ` x ) )
9	4, 8	syl6bb 276	1 |- ( ( F Fn A /\ G Fn A ) -> ( F = G <-> A. x e. A ( F ` x ) = ( G ` x ) ) )

Syntax hints:   -> wi 4   <-> wb 196   /\ wa 384   = wceq 1483   e. wcel 1990   A.wral 2912   _Vcvv 3200   |-> cmpt 4729   Fn wfn 5883   ` cfv 5888

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-opab 4713  df-mpt 4730  df-id 5024  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-iota 5851  df-fun 5890  df-fn 5891  df-fv 5896

This theorem is referenced by:  eqfnfv2  6312  eqfnfvd  6314  eqfnfv2f  6315  fvreseq0  6317  fnmptfvd  6320  fndmdifeq0  6323  fneqeql  6325  fnnfpeq0  6444  fconst2g  6468  cocan1  6546  cocan2  6547  weniso  6604  fnsuppres  7322  tfr3  7495  ixpfi2  8264  fipreima  8272  fseqenlem1  8847  fpwwe2lem8  9459  ofsubeq0  11017  ser0f  12854  hashgval2  13167  hashf1lem1  13239  prodf1f  14624  efcvgfsum  14816  prmreclem2  15621  1arithlem4  15630  1arith  15631  isgrpinv  17472  dprdf11  18422  psrbagconf1o  19374  islindf4  20177  pthaus  21441  xkohaus  21456  cnmpt11  21466  cnmpt21  21474  prdsxmetlem  22173  rrxmet  23191  rolle  23753  tdeglem4  23820  resinf1o  24282  dchrelbas2  24962  dchreq  24983  eqeefv  25783  axlowdimlem14  25835  nmlno0lem  27648  phoeqi  27713  occllem  28162  dfiop2  28612  hoeq  28619  ho01i  28687  hoeq1  28689  kbpj  28815  nmlnop0iALT  28854  lnopco0i  28863  nlelchi  28920  rnbra  28966  kbass5  28979  hmopidmchi  29010  hmopidmpji  29011  pjssdif2i  29033  pjinvari  29050  bnj1542  30927  bnj580  30983  subfacp1lem3  31164  subfacp1lem5  31166  mrsubff1  31411  msubff1  31453  faclimlem1  31629  fprb  31669  rdgprc  31700  broucube  33443  cocanfo  33512  eqfnun  33516  sdclem2  33538  rrnmet  33628  rrnequiv  33634  ltrnid  35421  ltrneq2  35434  tendoeq1  36052  pw2f1ocnv  37604  caofcan  38522  addrcom  38679  fsneq  39398  dvnprodlem1  40161