Theorem eqfnfv 7033

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 6951	. . 3 ⊢ (𝐹 Fn 𝐴 ↔ 𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)))
2		dffn5 6951	. . 3 ⊢ (𝐺 Fn 𝐴 ↔ 𝐺 = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥)))
3		eqeq12 2750	. . 3 ⊢ ((𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) ∧ 𝐺 = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥))) → (𝐹 = 𝐺 ↔ (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥))))
4	1, 2, 3	syl2anb 599	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) → (𝐹 = 𝐺 ↔ (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥))))
5		fvex 6905	. . . 4 ⊢ (𝐹‘𝑥) ∈ V
6	5	rgenw 3066	. . 3 ⊢ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ V
7		mpteqb 7018	. . 3 ⊢ (∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ V → ((𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥)) ↔ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = (𝐺‘𝑥)))
8	6, 7	ax-mp 5	. 2 ⊢ ((𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥)) ↔ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = (𝐺‘𝑥))
9	4, 8	bitrdi 287	1 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) → (𝐹 = 𝐺 ↔ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = (𝐺‘𝑥)))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 397   = wceq 1542   ∈ wcel 2107  ∀wral 3062  Vcvv 3475   ↦ cmpt 5232   Fn wfn 6539  ‘cfv 6544

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5300  ax-nul 5307  ax-pr 5428

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-br 5150  df-opab 5212  df-mpt 5233  df-id 5575  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-iota 6496  df-fun 6546  df-fn 6547  df-fv 6552

This theorem is referenced by:  eqfnfv2  7034  eqfnfvd  7036  eqfnfv2f  7037  eqfnun  7039  fvreseq0  7040  fnmptfvd  7043  fndmdifeq0  7046  fneqeql  7048  fnnfpeq0  7176  fprb  7195  fconst2g  7204  cocan1  7289  cocan2  7290  weniso  7351  fsplitfpar  8104  fnsuppres  8176  tfr3  8399  ixpfi2  9350  fipreima  9358  updjud  9929  fseqenlem1  10019  fpwwe2lem7  10632  ofsubeq0  12209  ser0f  14021  hashgval2  14338  hashf1lem1  14415  hashf1lem1OLD  14416  prodf1f  15838  efcvgfsum  16029  prmreclem2  16850  1arithlem4  16859  1arith  16860  smndex1n0mnd  18793  isgrpinv  18878  dprdf11  19893  frlmplusgvalb  21324  frlmvscavalb  21325  islindf4  21393  psrbagconf1o  21489  psrbagconf1oOLD  21490  pthaus  23142  xkohaus  23157  cnmpt11  23167  cnmpt21  23175  prdsxmetlem  23874  rrxmet  24925  rolle  25507  tdeglem4  25577  tdeglem4OLD  25578  resinf1o  26045  dchrelbas2  26740  dchreq  26761  eqeefv  28161  axlowdimlem14  28213  elntg2  28243  nmlno0lem  30046  phoeqi  30110  occllem  30556  dfiop2  31006  hoeq  31013  ho01i  31081  hoeq1  31083  kbpj  31209  nmlnop0iALT  31248  lnopco0i  31257  nlelchi  31314  rnbra  31360  kbass5  31373  hmopidmchi  31404  hmopidmpji  31405  pjssdif2i  31427  pjinvari  31444  bnj1542  33868  bnj580  33924  subfacp1lem3  34173  subfacp1lem5  34175  mrsubff1  34505  msubff1  34547  faclimlem1  34713  rdgprc  34766  broucube  36522  cocanfo  36587  sdclem2  36610  rrnmet  36697  rrnequiv  36703  ltrnid  39006  ltrneq2  39019  tendoeq1  39635  sticksstones1  40962  pw2f1ocnv  41776  caofcan  43082  addrcom  43234  fsneq  43905  dvnprodlem1  44662  cfsetsnfsetf1  45769  cfsetsnfsetfo  45770  rrx2pnecoorneor  47401  rrx2linest  47428