Theorem eqfnfv 7020

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 6936	. . 3 ⊢ (𝐹 Fn 𝐴 ↔ 𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)))
2		dffn5 6936	. . 3 ⊢ (𝐺 Fn 𝐴 ↔ 𝐺 = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥)))
3		eqeq12 2752	. . 3 ⊢ ((𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) ∧ 𝐺 = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥))) → (𝐹 = 𝐺 ↔ (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥))))
4	1, 2, 3	syl2anb 598	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) → (𝐹 = 𝐺 ↔ (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥))))
5		fvex 6888	. . . 4 ⊢ (𝐹‘𝑥) ∈ V
6	5	rgenw 3055	. . 3 ⊢ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ V
7		mpteqb 7004	. . 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 2108  ∀wral 3051  Vcvv 3459   ↦ cmpt 5201   Fn wfn 6525  ‘cfv 6530

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 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pr 5402

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 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2809  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3061  df-rab 3416  df-v 3461  df-sbc 3766  df-csb 3875  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-opab 5182  df-mpt 5202  df-id 5548  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-res 5666  df-ima 5667  df-iota 6483  df-fun 6532  df-fn 6533  df-fv 6538

This theorem is referenced by:  eqfnfv2  7021  eqfnfvd  7023  eqfnfv2f  7024  eqfnun  7026  fvreseq0  7027  fnmptfvd  7030  fndmdifeq0  7033  fneqeql  7035  fnnfpeq0  7169  fprb  7185  fconst2g  7194  cocan1  7283  cocan2  7284  weniso  7346  fsplitfpar  8115  fnsuppres  8188  tfr3  8411  ixpfi2  9360  fipreima  9368  updjud  9946  fseqenlem1  10036  fpwwe2lem7  10649  ofsubeq0  12235  ser0f  14071  hashgval2  14394  hashf1lem1  14471  prodf1f  15906  efcvgfsum  16100  prmreclem2  16935  1arithlem4  16944  1arith  16945  smndex1n0mnd  18888  isgrpinv  18974  dprdf11  20004  frlmplusgvalb  21727  frlmvscavalb  21728  islindf4  21796  psrbagconf1o  21887  pthaus  23574  xkohaus  23589  cnmpt11  23599  cnmpt21  23607  prdsxmetlem  24305  rrxmet  25358  rolle  25944  tdeglem4  26015  resinf1o  26495  dchrelbas2  27198  dchreq  27219  eqeefv  28828  axlowdimlem14  28880  elntg2  28910  nmlno0lem  30720  phoeqi  30784  occllem  31230  dfiop2  31680  hoeq  31687  ho01i  31755  hoeq1  31757  kbpj  31883  nmlnop0iALT  31922  lnopco0i  31931  nlelchi  31988  rnbra  32034  kbass5  32047  hmopidmchi  32078  hmopidmpji  32079  pjssdif2i  32101  pjinvari  32118  bnj1542  34834  bnj580  34890  subfacp1lem3  35150  subfacp1lem5  35152  mrsubff1  35482  msubff1  35524  faclimlem1  35706  rdgprc  35758  broucube  37624  cocanfo  37689  sdclem2  37712  rrnmet  37799  rrnequiv  37805  ltrnid  40100  ltrneq2  40113  tendoeq1  40729  sticksstones1  42105  pw2f1ocnv  43008  caofcan  44295  addrcom  44447  fsneq  45178  dvnprodlem1  45923  cfsetsnfsetf1  47036  cfsetsnfsetfo  47037  rrx2pnecoorneor  48643  rrx2linest  48670  dfinito4  49334