Theorem eqfnfv 7025

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 6939	. . 3 ⊢ (𝐹 Fn 𝐴 ↔ 𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)))
2		dffn5 6939	. . 3 ⊢ (𝐺 Fn 𝐴 ↔ 𝐺 = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥)))
3		eqeq12 2780	. . 3 ⊢ ((𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) ∧ 𝐺 = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥))) → (𝐹 = 𝐺 ↔ (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥))))
4	1, 2, 3	syl2anb 609	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) → (𝐹 = 𝐺 ↔ (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥))))
5		fvex 6894	. . . 4 ⊢ (𝐹‘𝑥) ∈ V
6	5	rgenw 3083	. . 3 ⊢ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ V
7		mpteqb 7009	. . 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 1570   ∈ wcel 2143  ∀wral 3079  Vcvv 3455   ↦ cmpt 5192   Fn wfn 6531  ‘cfv 6536

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5257  ax-nul 5269  ax-pr 5404

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-sbc 3745  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4488  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-br 5110  df-opab 5174  df-mpt 5193  df-id 5556  df-xp 5667  df-rel 5668  df-cnv 5669  df-co 5670  df-dm 5671  df-rn 5672  df-res 5673  df-ima 5674  df-iota 6492  df-fun 6538  df-fn 6539  df-fv 6544

This theorem is referenced by:  eqfnfv2  7026  eqfnfvd  7028  eqfnfv2f  7029  fsneq  7030  eqfnun  7032  fvreseq0  7033  fnmptfvd  7036  fndmdifeq0  7039  fneqeql  7041  fnnfpeq0  7176  fprb  7192  fconst2g  7201  cocan1  7289  cocan2  7290  weniso  7352  fsplitfpar  8109  fnsuppres  8183  tfr3  8382  ixpfi2  9303  fipreima  9311  updjud  9916  fseqenlem1  10004  fpwwe2lem7  10617  ofsubeq0  12210  ser0f  14087  hashgval2  14410  hashf1lem1  14488  prodf1f  15942  efcvgfsum  16135  prmreclem2  16972  1arithlem4  16981  1arith  16982  smndex1n0mnd  18969  isgrpinv  19055  dprdf11  20090  frlmplusgvalb  21919  frlmvscavalb  21920  islindf4  21988  psrbagconf1o  22079  pthaus  23795  xkohaus  23810  cnmpt11  23820  cnmpt21  23828  prdsxmetlem  24525  rrxmet  25567  rolle  26149  tdeglem4  26217  resinf1o  26701  dchrelbas2  27401  dchreq  27422  eqeefv  29253  axlowdimlem14  29305  elntg2  29335  nmlno0lem  31145  phoeqi  31209  occllem  31655  dfiop2  32105  hoeq  32112  ho01i  32180  hoeq1  32182  kbpj  32308  nmlnop0iALT  32347  lnopco0i  32356  nlelchi  32413  rnbra  32459  kbass5  32472  hmopidmchi  32503  hmopidmpji  32504  pjssdif2i  32526  pjinvari  32543  bnj1542  35245  bnj580  35301  subfacp1lem3  35674  subfacp1lem5  35676  mrsubff1  36006  msubff1  36048  faclimlem1  36235  rdgprc  36284  broucube  38325  cocanfo  38390  sdclem2  38413  rrnmet  38500  rrnequiv  38506  ltrnid  40929  ltrneq2  40942  tendoeq1  41558  sticksstones1  42933  pw2f1ocnv  43784  caofcan  45053  addrcom  45203  dvnprodlem1  46680  cfsetsnfsetf1  47816  cfsetsnfsetfo  47817  rrx2pnecoorneor  49515  rrx2linest  49542  dfinito4  50299