Theorem eqfnfv 7006

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 6922	. . 3 ⊢ (𝐹 Fn 𝐴 ↔ 𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)))
2		dffn5 6922	. . 3 ⊢ (𝐺 Fn 𝐴 ↔ 𝐺 = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥)))
3		eqeq12 2747	. . 3 ⊢ ((𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) ∧ 𝐺 = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥))) → (𝐹 = 𝐺 ↔ (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥))))
4	1, 2, 3	syl2anb 598	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) → (𝐹 = 𝐺 ↔ (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥))))
5		fvex 6874	. . . 4 ⊢ (𝐹‘𝑥) ∈ V
6	5	rgenw 3049	. . 3 ⊢ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ V
7		mpteqb 6990	. . 3 ⊢ (∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ V → ((𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥)) ↔ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = (𝐺‘𝑥)))
8	6, 7	ax-mp 5	. 2 ⊢ ((𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥)) ↔ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = (𝐺‘𝑥))
9	4, 8	bitrdi 287	1 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) → (𝐹 = 𝐺 ↔ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = (𝐺‘𝑥)))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1540   ∈ wcel 2109  ∀wral 3045  Vcvv 3450   ↦ cmpt 5191   Fn wfn 6509  ‘cfv 6514

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-sep 5254  ax-nul 5264  ax-pr 5390

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-sbc 3757  df-csb 3866  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-opab 5173  df-mpt 5192  df-id 5536  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-res 5653  df-ima 5654  df-iota 6467  df-fun 6516  df-fn 6517  df-fv 6522

This theorem is referenced by:  eqfnfv2  7007  eqfnfvd  7009  eqfnfv2f  7010  eqfnun  7012  fvreseq0  7013  fnmptfvd  7016  fndmdifeq0  7019  fneqeql  7021  fnnfpeq0  7155  fprb  7171  fconst2g  7180  cocan1  7269  cocan2  7270  weniso  7332  fsplitfpar  8100  fnsuppres  8173  tfr3  8370  ixpfi2  9308  fipreima  9316  updjud  9894  fseqenlem1  9984  fpwwe2lem7  10597  ofsubeq0  12190  ser0f  14027  hashgval2  14350  hashf1lem1  14427  prodf1f  15865  efcvgfsum  16059  prmreclem2  16895  1arithlem4  16904  1arith  16905  smndex1n0mnd  18846  isgrpinv  18932  dprdf11  19962  frlmplusgvalb  21685  frlmvscavalb  21686  islindf4  21754  psrbagconf1o  21845  pthaus  23532  xkohaus  23547  cnmpt11  23557  cnmpt21  23565  prdsxmetlem  24263  rrxmet  25315  rolle  25901  tdeglem4  25972  resinf1o  26452  dchrelbas2  27155  dchreq  27176  eqeefv  28837  axlowdimlem14  28889  elntg2  28919  nmlno0lem  30729  phoeqi  30793  occllem  31239  dfiop2  31689  hoeq  31696  ho01i  31764  hoeq1  31766  kbpj  31892  nmlnop0iALT  31931  lnopco0i  31940  nlelchi  31997  rnbra  32043  kbass5  32056  hmopidmchi  32087  hmopidmpji  32088  pjssdif2i  32110  pjinvari  32127  bnj1542  34854  bnj580  34910  subfacp1lem3  35176  subfacp1lem5  35178  mrsubff1  35508  msubff1  35550  faclimlem1  35737  rdgprc  35789  broucube  37655  cocanfo  37720  sdclem2  37743  rrnmet  37830  rrnequiv  37836  ltrnid  40136  ltrneq2  40149  tendoeq1  40765  sticksstones1  42141  pw2f1ocnv  43033  caofcan  44319  addrcom  44471  fsneq  45207  dvnprodlem1  45951  cfsetsnfsetf1  47064  cfsetsnfsetfo  47065  rrx2pnecoorneor  48708  rrx2linest  48735  dfinito4  49494