Theorem eqfnfv 7043

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	⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) → (𝐹 = 𝐺 ↔ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = (𝐺‘𝑥)))

Distinct variable groups:   𝑥,𝐴   𝑥,𝐹   𝑥,𝐺

Proof of Theorem eqfnfv

Step	Hyp	Ref	Expression
1		dffn5 6960	. . 3 ⊢ (𝐹 Fn 𝐴 ↔ 𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)))
2		dffn5 6960	. . 3 ⊢ (𝐺 Fn 𝐴 ↔ 𝐺 = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥)))
3		eqeq12 2744	. . 3 ⊢ ((𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) ∧ 𝐺 = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥))) → (𝐹 = 𝐺 ↔ (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥))))
4	1, 2, 3	syl2anb 596	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) → (𝐹 = 𝐺 ↔ (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥))))
5		fvex 6913	. . . 4 ⊢ (𝐹‘𝑥) ∈ V
6	5	rgenw 3061	. . 3 ⊢ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ V
7		mpteqb 7027	. . 3 ⊢ (∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ V → ((𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥)) ↔ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = (𝐺‘𝑥)))
8	6, 7	ax-mp 5	. 2 ⊢ ((𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥)) ↔ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = (𝐺‘𝑥))
9	4, 8	bitrdi 286	1 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) → (𝐹 = 𝐺 ↔ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = (𝐺‘𝑥)))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 394   = wceq 1533   ∈ wcel 2098  ∀wral 3057  Vcvv 3471   ↦ cmpt 5233   Fn wfn 6546  ‘cfv 6551

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2698  ax-sep 5301  ax-nul 5308  ax-pr 5431

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2529  df-eu 2558  df-clab 2705  df-cleq 2719  df-clel 2805  df-nfc 2880  df-ne 2937  df-ral 3058  df-rex 3067  df-rab 3429  df-v 3473  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4325  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4911  df-br 5151  df-opab 5213  df-mpt 5234  df-id 5578  df-xp 5686  df-rel 5687  df-cnv 5688  df-co 5689  df-dm 5690  df-rn 5691  df-res 5692  df-ima 5693  df-iota 6503  df-fun 6553  df-fn 6554  df-fv 6559

This theorem is referenced by:  eqfnfv2  7044  eqfnfvd  7046  eqfnfv2f  7047  eqfnun  7049  fvreseq0  7050  fnmptfvd  7053  fndmdifeq0  7056  fneqeql  7058  fnnfpeq0  7191  fprb  7210  fconst2g  7219  cocan1  7304  cocan2  7305  weniso  7366  fsplitfpar  8127  fnsuppres  8200  tfr3  8424  ixpfi2  9380  fipreima  9388  updjud  9963  fseqenlem1  10053  fpwwe2lem7  10666  ofsubeq0  12245  ser0f  14058  hashgval2  14375  hashf1lem1  14453  hashf1lem1OLD  14454  prodf1f  15876  efcvgfsum  16068  prmreclem2  16891  1arithlem4  16900  1arith  16901  smndex1n0mnd  18869  isgrpinv  18955  dprdf11  19985  frlmplusgvalb  21708  frlmvscavalb  21709  islindf4  21777  psrbagconf1o  21875  psrbagconf1oOLD  21876  pthaus  23560  xkohaus  23575  cnmpt11  23585  cnmpt21  23593  prdsxmetlem  24292  rrxmet  25354  rolle  25940  tdeglem4  26013  tdeglem4OLD  26014  resinf1o  26488  dchrelbas2  27188  dchreq  27209  eqeefv  28732  axlowdimlem14  28784  elntg2  28814  nmlno0lem  30621  phoeqi  30685  occllem  31131  dfiop2  31581  hoeq  31588  ho01i  31656  hoeq1  31658  kbpj  31784  nmlnop0iALT  31823  lnopco0i  31832  nlelchi  31889  rnbra  31935  kbass5  31948  hmopidmchi  31979  hmopidmpji  31980  pjssdif2i  32002  pjinvari  32019  bnj1542  34493  bnj580  34549  subfacp1lem3  34797  subfacp1lem5  34799  mrsubff1  35129  msubff1  35171  faclimlem1  35342  rdgprc  35395  broucube  37132  cocanfo  37197  sdclem2  37220  rrnmet  37307  rrnequiv  37313  ltrnid  39612  ltrneq2  39625  tendoeq1  40241  sticksstones1  41622  pw2f1ocnv  42461  caofcan  43763  addrcom  43915  fsneq  44582  dvnprodlem1  45336  cfsetsnfsetf1  46443  cfsetsnfsetfo  46444  rrx2pnecoorneor  47839  rrx2linest  47866