Theorem eqfnfv 6976

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 6892	. . 3 ⊢ (𝐹 Fn 𝐴 ↔ 𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)))
2		dffn5 6892	. . 3 ⊢ (𝐺 Fn 𝐴 ↔ 𝐺 = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥)))
3		eqeq12 2753	. . 3 ⊢ ((𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) ∧ 𝐺 = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥))) → (𝐹 = 𝐺 ↔ (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥))))
4	1, 2, 3	syl2anb 598	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) → (𝐹 = 𝐺 ↔ (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥))))
5		fvex 6847	. . . 4 ⊢ (𝐹‘𝑥) ∈ V
6	5	rgenw 3055	. . 3 ⊢ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ V
7		mpteqb 6960	. . 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 1541   ∈ wcel 2113  ∀wral 3051  Vcvv 3440   ↦ cmpt 5179   Fn wfn 6487  ‘cfv 6492

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2184  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pr 5377

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3061  df-rab 3400  df-v 3442  df-sbc 3741  df-csb 3850  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-uni 4864  df-br 5099  df-opab 5161  df-mpt 5180  df-id 5519  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-iota 6448  df-fun 6494  df-fn 6495  df-fv 6500

This theorem is referenced by:  eqfnfv2  6977  eqfnfvd  6979  eqfnfv2f  6980  eqfnun  6982  fvreseq0  6983  fnmptfvd  6986  fndmdifeq0  6989  fneqeql  6991  fnnfpeq0  7124  fprb  7140  fconst2g  7149  cocan1  7237  cocan2  7238  weniso  7300  fsplitfpar  8060  fnsuppres  8133  tfr3  8330  ixpfi2  9250  fipreima  9258  updjud  9846  fseqenlem1  9934  fpwwe2lem7  10548  ofsubeq0  12142  ser0f  13978  hashgval2  14301  hashf1lem1  14378  prodf1f  15815  efcvgfsum  16009  prmreclem2  16845  1arithlem4  16854  1arith  16855  smndex1n0mnd  18837  isgrpinv  18923  dprdf11  19954  frlmplusgvalb  21724  frlmvscavalb  21725  islindf4  21793  psrbagconf1o  21885  pthaus  23582  xkohaus  23597  cnmpt11  23607  cnmpt21  23615  prdsxmetlem  24312  rrxmet  25364  rolle  25950  tdeglem4  26021  resinf1o  26501  dchrelbas2  27204  dchreq  27225  eqeefv  28976  axlowdimlem14  29028  elntg2  29058  nmlno0lem  30868  phoeqi  30932  occllem  31378  dfiop2  31828  hoeq  31835  ho01i  31903  hoeq1  31905  kbpj  32031  nmlnop0iALT  32070  lnopco0i  32079  nlelchi  32136  rnbra  32182  kbass5  32195  hmopidmchi  32226  hmopidmpji  32227  pjssdif2i  32249  pjinvari  32266  bnj1542  35013  bnj580  35069  subfacp1lem3  35376  subfacp1lem5  35378  mrsubff1  35708  msubff1  35750  faclimlem1  35937  rdgprc  35986  broucube  37855  cocanfo  37920  sdclem2  37943  rrnmet  38030  rrnequiv  38036  ltrnid  40405  ltrneq2  40418  tendoeq1  41034  sticksstones1  42410  pw2f1ocnv  43289  caofcan  44574  addrcom  44725  fsneq  45460  dvnprodlem1  46200  cfsetsnfsetf1  47315  cfsetsnfsetfo  47316  rrx2pnecoorneor  48971  rrx2linest  48998  dfinito4  49756