Theorem eqfnfv 6985

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 6901	. . 3 ⊢ (𝐹 Fn 𝐴 ↔ 𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)))
2		dffn5 6901	. . 3 ⊢ (𝐺 Fn 𝐴 ↔ 𝐺 = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥)))
3		eqeq12 2746	. . 3 ⊢ ((𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) ∧ 𝐺 = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥))) → (𝐹 = 𝐺 ↔ (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥))))
4	1, 2, 3	syl2anb 598	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) → (𝐹 = 𝐺 ↔ (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥))))
5		fvex 6853	. . . 4 ⊢ (𝐹‘𝑥) ∈ V
6	5	rgenw 3048	. . 3 ⊢ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ V
7		mpteqb 6969	. . 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 3044  Vcvv 3444   ↦ cmpt 5183   Fn wfn 6494  ‘cfv 6499

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 2701  ax-sep 5246  ax-nul 5256  ax-pr 5382

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 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-rab 3403  df-v 3446  df-sbc 3751  df-csb 3860  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5103  df-opab 5165  df-mpt 5184  df-id 5526  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-iota 6452  df-fun 6501  df-fn 6502  df-fv 6507

This theorem is referenced by:  eqfnfv2  6986  eqfnfvd  6988  eqfnfv2f  6989  eqfnun  6991  fvreseq0  6992  fnmptfvd  6995  fndmdifeq0  6998  fneqeql  7000  fnnfpeq0  7134  fprb  7150  fconst2g  7159  cocan1  7248  cocan2  7249  weniso  7311  fsplitfpar  8074  fnsuppres  8147  tfr3  8344  ixpfi2  9277  fipreima  9285  updjud  9863  fseqenlem1  9953  fpwwe2lem7  10566  ofsubeq0  12159  ser0f  13996  hashgval2  14319  hashf1lem1  14396  prodf1f  15834  efcvgfsum  16028  prmreclem2  16864  1arithlem4  16873  1arith  16874  smndex1n0mnd  18821  isgrpinv  18907  dprdf11  19939  frlmplusgvalb  21711  frlmvscavalb  21712  islindf4  21780  psrbagconf1o  21871  pthaus  23558  xkohaus  23573  cnmpt11  23583  cnmpt21  23591  prdsxmetlem  24289  rrxmet  25341  rolle  25927  tdeglem4  25998  resinf1o  26478  dchrelbas2  27181  dchreq  27202  eqeefv  28883  axlowdimlem14  28935  elntg2  28965  nmlno0lem  30772  phoeqi  30836  occllem  31282  dfiop2  31732  hoeq  31739  ho01i  31807  hoeq1  31809  kbpj  31935  nmlnop0iALT  31974  lnopco0i  31983  nlelchi  32040  rnbra  32086  kbass5  32099  hmopidmchi  32130  hmopidmpji  32131  pjssdif2i  32153  pjinvari  32170  bnj1542  34840  bnj580  34896  subfacp1lem3  35162  subfacp1lem5  35164  mrsubff1  35494  msubff1  35536  faclimlem1  35723  rdgprc  35775  broucube  37641  cocanfo  37706  sdclem2  37729  rrnmet  37816  rrnequiv  37822  ltrnid  40122  ltrneq2  40135  tendoeq1  40751  sticksstones1  42127  pw2f1ocnv  43019  caofcan  44305  addrcom  44457  fsneq  45193  dvnprodlem1  45937  cfsetsnfsetf1  47053  cfsetsnfsetfo  47054  rrx2pnecoorneor  48697  rrx2linest  48724  dfinito4  49483