Theorem eqfnfv 7026

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 6940	. . 3 ⊢ (𝐹 Fn 𝐴 ↔ 𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)))
2		dffn5 6940	. . 3 ⊢ (𝐺 Fn 𝐴 ↔ 𝐺 = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥)))
3		eqeq12 2786	. . 3 ⊢ ((𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) ∧ 𝐺 = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥))) → (𝐹 = 𝐺 ↔ (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥))))
4	1, 2, 3	syl2anb 609	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) → (𝐹 = 𝐺 ↔ (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥))))
5		fvex 6895	. . . 4 ⊢ (𝐹‘𝑥) ∈ V
6	5	rgenw 3089	. . 3 ⊢ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ V
7		mpteqb 7010	. . 3 ⊢ (∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ V → ((𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥)) ↔ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = (𝐺‘𝑥)))
8	6, 7	ax-mp 5	. 2 ⊢ ((𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥)) ↔ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = (𝐺‘𝑥))
9	4, 8	bitrdi 290	1 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) → (𝐹 = 𝐺 ↔ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = (𝐺‘𝑥)))

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400   = wceq 1567   ∈ wcel 2149  ∀wral 3085  Vcvv 3463   ↦ cmpt 5196   Fn wfn 6532  ‘cfv 6537

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-sep 5261  ax-nul 5271  ax-pr 5405

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ne 2965  df-ral 3086  df-rex 3096  df-rab 3424  df-v 3465  df-sbc 3754  df-csb 3862  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4877  df-br 5114  df-opab 5178  df-mpt 5197  df-id 5557  df-xp 5668  df-rel 5669  df-cnv 5670  df-co 5671  df-dm 5672  df-rn 5673  df-res 5674  df-ima 5675  df-iota 6493  df-fun 6539  df-fn 6540  df-fv 6545

This theorem is referenced by:  eqfnfv2  7027  eqfnfvd  7029  eqfnfv2f  7030  fsneq  7031  eqfnun  7033  fvreseq0  7034  fnmptfvd  7037  fndmdifeq0  7040  fneqeql  7042  fnnfpeq0  7177  fprb  7193  fconst2g  7202  cocan1  7290  cocan2  7291  weniso  7353  fsplitfpar  8113  fnsuppres  8187  tfr3  8386  ixpfi2  9307  fipreima  9315  updjud  9920  fseqenlem1  10008  fpwwe2lem7  10622  ofsubeq0  12215  ser0f  14091  hashgval2  14414  hashf1lem1  14492  prodf1f  15946  efcvgfsum  16140  prmreclem2  16977  1arithlem4  16986  1arith  16987  smndex1n0mnd  18974  isgrpinv  19060  dprdf11  20095  frlmplusgvalb  21888  frlmvscavalb  21889  islindf4  21957  psrbagconf1o  22048  pthaus  23764  xkohaus  23779  cnmpt11  23789  cnmpt21  23797  prdsxmetlem  24494  rrxmet  25536  rolle  26118  tdeglem4  26186  resinf1o  26667  dchrelbas2  27367  dchreq  27388  eqeefv  29194  axlowdimlem14  29246  elntg2  29276  nmlno0lem  31086  phoeqi  31150  occllem  31596  dfiop2  32046  hoeq  32053  ho01i  32121  hoeq1  32123  kbpj  32249  nmlnop0iALT  32288  lnopco0i  32297  nlelchi  32354  rnbra  32400  kbass5  32413  hmopidmchi  32444  hmopidmpji  32445  pjssdif2i  32467  pjinvari  32484  bnj1542  35190  bnj580  35246  subfacp1lem3  35573  subfacp1lem5  35575  mrsubff1  35905  msubff1  35947  faclimlem1  36134  rdgprc  36183  broucube  38193  cocanfo  38258  sdclem2  38281  rrnmet  38368  rrnequiv  38374  ltrnid  40799  ltrneq2  40812  tendoeq1  41428  sticksstones1  42803  pw2f1ocnv  43656  caofcan  44925  addrcom  45075  dvnprodlem1  46552  cfsetsnfsetf1  47685  cfsetsnfsetfo  47686  rrx2pnecoorneor  49380  rrx2linest  49407  dfinito4  50164