Theorem eqfnfv 7003

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 6919	. . 3 ⊢ (𝐹 Fn 𝐴 ↔ 𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)))
2		dffn5 6919	. . 3 ⊢ (𝐺 Fn 𝐴 ↔ 𝐺 = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥)))
3		eqeq12 2746	. . 3 ⊢ ((𝐹 = (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) ∧ 𝐺 = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥))) → (𝐹 = 𝐺 ↔ (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥))))
4	1, 2, 3	syl2anb 598	. 2 ⊢ ((𝐹 Fn 𝐴 ∧ 𝐺 Fn 𝐴) → (𝐹 = 𝐺 ↔ (𝑥 ∈ 𝐴 ↦ (𝐹‘𝑥)) = (𝑥 ∈ 𝐴 ↦ (𝐺‘𝑥))))
5		fvex 6871	. . . 4 ⊢ (𝐹‘𝑥) ∈ V
6	5	rgenw 3048	. . 3 ⊢ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ V
7		mpteqb 6987	. . 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 3447   ↦ cmpt 5188   Fn wfn 6506  ‘cfv 6511

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 5251  ax-nul 5261  ax-pr 5387

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 3406  df-v 3449  df-sbc 3754  df-csb 3863  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-opab 5170  df-mpt 5189  df-id 5533  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 6464  df-fun 6513  df-fn 6514  df-fv 6519

This theorem is referenced by:  eqfnfv2  7004  eqfnfvd  7006  eqfnfv2f  7007  eqfnun  7009  fvreseq0  7010  fnmptfvd  7013  fndmdifeq0  7016  fneqeql  7018  fnnfpeq0  7152  fprb  7168  fconst2g  7177  cocan1  7266  cocan2  7267  weniso  7329  fsplitfpar  8097  fnsuppres  8170  tfr3  8367  ixpfi2  9301  fipreima  9309  updjud  9887  fseqenlem1  9977  fpwwe2lem7  10590  ofsubeq0  12183  ser0f  14020  hashgval2  14343  hashf1lem1  14420  prodf1f  15858  efcvgfsum  16052  prmreclem2  16888  1arithlem4  16897  1arith  16898  smndex1n0mnd  18839  isgrpinv  18925  dprdf11  19955  frlmplusgvalb  21678  frlmvscavalb  21679  islindf4  21747  psrbagconf1o  21838  pthaus  23525  xkohaus  23540  cnmpt11  23550  cnmpt21  23558  prdsxmetlem  24256  rrxmet  25308  rolle  25894  tdeglem4  25965  resinf1o  26445  dchrelbas2  27148  dchreq  27169  eqeefv  28830  axlowdimlem14  28882  elntg2  28912  nmlno0lem  30722  phoeqi  30786  occllem  31232  dfiop2  31682  hoeq  31689  ho01i  31757  hoeq1  31759  kbpj  31885  nmlnop0iALT  31924  lnopco0i  31933  nlelchi  31990  rnbra  32036  kbass5  32049  hmopidmchi  32080  hmopidmpji  32081  pjssdif2i  32103  pjinvari  32120  bnj1542  34847  bnj580  34903  subfacp1lem3  35169  subfacp1lem5  35171  mrsubff1  35501  msubff1  35543  faclimlem1  35730  rdgprc  35782  broucube  37648  cocanfo  37713  sdclem2  37736  rrnmet  37823  rrnequiv  37829  ltrnid  40129  ltrneq2  40142  tendoeq1  40758  sticksstones1  42134  pw2f1ocnv  43026  caofcan  44312  addrcom  44464  fsneq  45200  dvnprodlem1  45944  cfsetsnfsetf1  47060  cfsetsnfsetfo  47061  rrx2pnecoorneor  48704  rrx2linest  48731  dfinito4  49490