Theorem eqfnfv 6987

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 6906	. . 3 ⊢ (𝐹 Fn 𝐴 ↔ 𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)))
2		dffn5 6906	. . 3 ⊢ (𝐺 Fn 𝐴 ↔ 𝐺 = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥)))
3		eqeq12 2748	. . 3 ⊢ ((𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) ∧ 𝐺 = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥))) → (𝐹 = 𝐺 ↔ (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥))))
4	1, 2, 3	syl2anb 598	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) → (𝐹 = 𝐺 ↔ (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥))))
5		fvex 6860	. . . 4 ⊢ (𝐹‘𝑥) ∈ V
6	5	rgenw 3064	. . 3 ⊢ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ V
7		mpteqb 6972	. . 3 ⊢ (∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ V → ((𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥)) ↔ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = (𝐺‘𝑥)))
8	6, 7	ax-mp 5	. 2 ⊢ ((𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥)) ↔ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = (𝐺‘𝑥))
9	4, 8	bitrdi 286	1 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) → (𝐹 = 𝐺 ↔ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) = (𝐺‘𝑥)))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   = wceq 1541   ∈ wcel 2106  ∀wral 3060  Vcvv 3446   ↦ cmpt 5193   Fn wfn 6496  ‘cfv 6501

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2702  ax-sep 5261  ax-nul 5268  ax-pr 5389

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-ral 3061  df-rex 3070  df-rab 3406  df-v 3448  df-sbc 3743  df-csb 3859  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4288  df-if 4492  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-br 5111  df-opab 5173  df-mpt 5194  df-id 5536  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-iota 6453  df-fun 6503  df-fn 6504  df-fv 6509

This theorem is referenced by:  eqfnfv2  6988  eqfnfvd  6990  eqfnfv2f  6991  fvreseq0  6993  fnmptfvd  6996  fndmdifeq0  6999  fneqeql  7001  fnnfpeq0  7129  fprb  7148  fconst2g  7157  cocan1  7242  cocan2  7243  weniso  7304  fsplitfpar  8055  fnsuppres  8127  tfr3  8350  ixpfi2  9301  fipreima  9309  updjud  9879  fseqenlem1  9969  fpwwe2lem7  10582  ofsubeq0  12159  ser0f  13971  hashgval2  14288  hashf1lem1  14365  hashf1lem1OLD  14366  prodf1f  15788  efcvgfsum  15979  prmreclem2  16800  1arithlem4  16809  1arith  16810  smndex1n0mnd  18736  isgrpinv  18818  dprdf11  19816  frlmplusgvalb  21212  frlmvscavalb  21213  islindf4  21281  psrbagconf1o  21375  psrbagconf1oOLD  21376  pthaus  23026  xkohaus  23041  cnmpt11  23051  cnmpt21  23059  prdsxmetlem  23758  rrxmet  24809  rolle  25391  tdeglem4  25461  tdeglem4OLD  25462  resinf1o  25929  dchrelbas2  26622  dchreq  26643  eqeefv  27915  axlowdimlem14  27967  elntg2  27997  nmlno0lem  29798  phoeqi  29862  occllem  30308  dfiop2  30758  hoeq  30765  ho01i  30833  hoeq1  30835  kbpj  30961  nmlnop0iALT  31000  lnopco0i  31009  nlelchi  31066  rnbra  31112  kbass5  31125  hmopidmchi  31156  hmopidmpji  31157  pjssdif2i  31179  pjinvari  31196  bnj1542  33558  bnj580  33614  subfacp1lem3  33863  subfacp1lem5  33865  mrsubff1  34195  msubff1  34237  faclimlem1  34402  rdgprc  34455  broucube  36185  cocanfo  36250  eqfnun  36254  sdclem2  36274  rrnmet  36361  rrnequiv  36367  ltrnid  38671  ltrneq2  38684  tendoeq1  39300  sticksstones1  40627  pw2f1ocnv  41419  caofcan  42725  addrcom  42877  fsneq  43548  dvnprodlem1  44307  cfsetsnfsetf1  45413  cfsetsnfsetfo  45414  rrx2pnecoorneor  46921  rrx2linest  46948